∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↥X),
  (CategoryTheory.ConcreteCategory.hom g.base) ((CategoryTheory.ConcreteCategory.hom f.base) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g).base) x