∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f]
  (x : ↥(AlgebraicGeometry.Scheme.Hom.image f)),
  Function.Injective
    ⇑(CategoryTheory.ConcreteCategory.hom
        ((TopCat.Presheaf.stalkFunctor CommRingCat x).map (AlgebraicGeometry.Scheme.Hom.toImage f).c))