The stalk of an associated sheaf is the localisation

Define $\phi$ on germs by choosing a distinguished open $D(f)\ni \mathfrak{p}$, that is $f\mathrm{\notin }\mathfrak{p}$, and an element $s\in M_f$ representing the germ; send it to the image of $s$ under the canonical localisation $M_f\to M_{\mathfrak{p}}$ of [F3], the element written $s\mathrm{/}1$. This is well defined: a germ has a representative on some distinguished $D(f)\ni \mathfrak{p}$ by [F2], any two such open sets $D(f),D(g)$ may be compared after passing to $D(fg)\ni \mathfrak{p}$, and on $D(fg)$ the compatibility law of [F4], $s{\mathrm{\mid }}_{D(fg)}={\rho }_{fg}(s)$, together with the factorisation $M_f\to M_{fg}\to M_{\mathfrak{p}}$ of localisations, shows that both choices give the same image in $M_{\mathfrak{p}}$.

The map $\phi$ is $A_{\mathfrak{p}}$-linear: the stalk $(\tilde{M}{)}_{\mathfrak{p}}$ is a module over ${\mathcal{O}}_{X,\mathfrak{p}}$, which is $A_{\mathfrak{p}}$ by [F3], and the localisation maps $M_f\to M_{\mathfrak{p}}$ are $A_f$-linear, hence $A_{\mathfrak{p}}$-linear on the colimit. Naturality in $M$ holds because $\tilde{u}$ has components $u_f$ on distinguished opens by [F1] and [F4], and $u_f$ is the localisation of $u$, so it commutes with the maps $M_f\to M_{\mathfrak{p}}$ and $N_f\to N_{\mathfrak{p}}$.

$\phi$ is surjective: every element of $M_{\mathfrak{p}}$ is of the form $m\mathrm{/}s$ with $s\mathrm{\notin }\mathfrak{p}$, hence lies in the image of the canonical map $M_s\to M_{\mathfrak{p}}$ by the fraction criterion of [F3]; the element $m\mathrm{/}s\in M_s=\tilde{M}(D(s))$ has a germ at $\mathfrak{p}$ that $\phi$ sends to $m\mathrm{/}s$.

$\phi$ is injective: let $s\in M_f$ with $f\mathrm{\notin }\mathfrak{p}$ have image $0$ in $M_{\mathfrak{p}}$. Write $s=m\mathrm{/}{f}^k$ by [F3]; its image in $M_{\mathfrak{p}}$ is $m\mathrm{/}{f}^k$, so by the fraction criterion there is $t\mathrm{\notin }\mathfrak{p}$ with $tm=0$. In the localization $M_{ft}$ the element $t$ is invertible, so $m=0$ there and hence $s=m\mathrm{/}{f}^k=0$ there. Since $ft\mathrm{\notin }\mathfrak{p}$, $D(ft)$ is a distinguished neighbourhood of $\mathfrak{p}$ on which $s$ restricts to zero; therefore its germ is zero.

Thus $\phi$ is a bijective $A_{\mathfrak{p}}$-linear map, hence an isomorphism of $A_{\mathfrak{p}}$-modules, and by step 1.2 it is natural in $M$. The Axiom of Choice is inherited from the existence theorem [F1], which supplies $\tilde{M}$; the remaining argument makes only finitely many choices of elements and exponents.