∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat),
  CategoryTheory.CategoryStruct.comp (Y.Γevaluation ((CategoryTheory.ConcreteCategory.hom f.base) x))
      (AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f x) =
    CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op ⊤)) (X.Γevaluation x)