∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : X.Opens)
  (hUV : V ≤ (TopologicalSpace.Opens.map f.base).obj U) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (Y.presheaf.obj (Opposite.op U)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp V.toSpecΓ
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appLE f U V hUV))
        h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.resLE f U V hUV)
      (CategoryTheory.CategoryStruct.comp U.toSpecΓ h)