∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom f)
      (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom g) =
    AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom (CategoryTheory.CategoryStruct.comp f g)