∀ {R : Type u} [inst : CommRing R] (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hxU : x ∈ U) {Z : CommRingCat}
  (h : (AlgebraicGeometry.structurePresheafInCommRingCat R).stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom (algebraMap R ((AlgebraicGeometry.structureSheafInType R R).val.obj (Opposite.op U))))
      (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.structurePresheafInCommRingCat R).germ U x hxU) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk R x) h