Regular functions on a principal open are the principal localization

Restriction $A\to {\mathcal{O}}_X(D(f))$ is a unital algebra map. The function $1\mathrm{/}f$ is regular on $D(f)$, so F6 extends restriction to the displayed map. If $a\mathrm{/}{f}^r$ maps to zero, $a$ vanishes on $D(f)$; hence $fa$ vanishes everywhere on $X$, since $f=0$ outside $D(f)$. F2 gives $fa=0$ in $A$, and F7 makes the fraction zero. This proves injectivity without cancellation in $A$.

Fix $s\in {\mathcal{O}}_X(D(f))$. At each point take a local expression $s=g\mathrm{/}h$ and refine its neighbourhood to $D(a)\subseteq D(f)\cap D(h)$ by F3. The inclusion $V_X(h)\subseteq V_X(a)$ gives $a\in \sqrt{(h)}$ by F1. Thus $a^e=hb$ for some $e\ge 1,b\in A$. On $D(a)$, set $t=a^e$ and $c=gb$; then $D(t)=D(a)$ and $s=c\mathrm{/}t$.

Consider the set of all pairs $(t,c)$ obtained in step 1.2; their opens $D(t)$ cover $D(f)$ and are contained in it. Thus $f$ vanishes on the simultaneous zero locus of the $t^2$. By F1, $f\in \sqrt{(t^2:(t,c)\text{ as above})}$. F8 supplies finitely many of these pairs $(t_i,c_i)$ and $u_i\in A$ with $f^N={\sum }_{i=1}^m{u}_i{t}_i^2$, for some $N\ge 1$. No compactness theorem or simultaneous choice of neighbourhoods is needed.

For $p\in D(f)$ and each selected pair, if $t_i(p)\mathrm{\ne }0$ then $c_i(p)=s(p)t_i(p)$; if $t_i(p)=0$ then both $c_i(p)t_i(p)$ and $s(p)t_i(p{)}^2$ are zero. Hence ${\sum }_i{u}_i(p)c_i(p)t_i(p)=s(p){\sum }_i{u}_i(p)t_i(p{)}^2=s(p)f(p{)}^N$. Division by the nonzero scalar $f(p{)}^N$ shows that $({\sum }_i{u}_i{c}_i{t}_i)\mathrm{/}{f}^N$ maps to $s$. This proves surjectivity.

If $D(f)$ is empty, $f$ is the zero function on $X$, hence zero in $A$ by F2. Localizing at 0 is the zero ring by F7; the empty domain has one function and its algebra is zero. If $f=1$, the same construction gives global sections and $A_1=A$. Together with injectivity and surjectivity this proves all cases.