∀ {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U)
  (hx : x ∈ V) {Z : CommRingCat} (h_1 : (X.restrict h).presheaf.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.presheaf.germ (⋯.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯)
      (CategoryTheory.CategoryStruct.comp (X.restrictStalkIso h x).inv h_1) =
    CategoryTheory.CategoryStruct.comp ((X.restrict h).presheaf.germ V x hx) h_1