∀ {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map g)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CategoryTheory.CategoryStruct.comp f g)) h