The classical affine local ring is localization at the point's maximal ideal

Each $s\mathrm{\notin }{\mathfrak{m}}_x$ has $s(x)\mathrm{\ne }0$ and the germ of $1\mathrm{/}s$ on $D(s)$ is its multiplicative inverse. F4 therefore defines the displayed map to the germ algebra. Every germ has a representative $g\mathrm{/}h$ near $x$ with $h(x)\mathrm{\ne }0$, so is in its image.

If $a\mathrm{/}s$ has zero germ, $a\mathrm{/}s$ vanishes on a neighbourhood of $x$ inside $D(s)$. F3 supplies $D(h)$ containing $x$ inside this neighbourhood. On $D(h)$ the numerator $a$ vanishes, and outside $D(h)$ the factor $h$ vanishes. Hence $ha=0$ as a function on $X$, and F7 makes it zero in $A$. Since $h(x)\mathrm{\ne }0$, F5 gives $a\mathrm{/}s=0$ in $A_{{\mathfrak{m}}_x}$. Thus the map is injective.

The ideal ${\mathfrak{m}}_x$ is prime: if $ab(x)=0$ in the field $k$, one factor evaluates to zero, and 1 does not. F6 applies and says the unique maximal ideal consists of $a\mathrm{/}s$ with $a(x)=0$. Because $s(x)\mathrm{\ne }0$, this is exactly the condition that its germ evaluates to zero. Evaluation is onto $k$ through constants and identifies its quotient with $k$, giving the residue-field assertion.