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