∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  {Z : AlgebraicGeometry.LocallyRingedSpace} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.isoRestrict f).hom
      (CategoryTheory.CategoryStruct.comp (Y.ofRestrict ⋯) h) =
    CategoryTheory.CategoryStruct.comp f h