Finite is affine and local on its target

If $f$ is finite, [F1] gives affine inverse images over every affine open of $S$, so [F2] says $f$ is affine. It also gives the stated condition on any affine open cover. This direction uses only the definition of finite.

Conversely, assume AC and the stated affine-cover condition. [F4] applies to the cover and shows that $f$ is affine. This is the first use of AC: it is confined to inferring global affineness from local affine inverse images.

Fix an arbitrary affine open $U=\mathrm{Spec}R\subseteq S$. By step 1.2, write $f^{-1}(U)=\mathrm{Spec}B$. If $U=\mathrm{\varnothing }$, then $B=0$ by the affine-scheme/ring correspondence [F7], so $B$ is finite over $R$; assume henceforth that $U$ is nonempty. The restricted affine morphism induces a ring map $R\to B$ by [F7].

Consider all pairs $(i,h)$ for which $U_i=\mathrm{Spec}{R}_i$ and the distinguished open $D_U(h)\subseteq U$ lies in $U_i$. These opens cover $U$: each $U\cap U_i$ is open in $U$, and [F6] supplies a distinguished-open neighbourhood of each of its points contained in that intersection. By [F5], choose a finite subcover $W_j=D_U(h_j)$, retaining for each selected member its cover index $i(j)$. The family of all such pairs was considered, so this finite subcover requires no simultaneous choice over the points of $U$.

Fix one selected $W_j$ and put $C_j=\mathrm{\Gamma }(W_j,{\mathcal{O}}_U)=R_{h_j}$ by [F8, F9]. Since $W_j\subseteq U_{i(j)}$, [F11] identifies $f^{-1}(W_j)$ with $f^{-1}(U_{i(j)}){\times }_{U_{i(j)}}{W}_j$. Both factors are affine, so [F10] identifies this inverse image with the spectrum of $B_{i(j)}{\otimes }_{R_{i(j)}}{C}_j$, where $f^{-1}(U_{i(j)})=\mathrm{Spec}{B}_{i(j)}$. The ring $B_{i(j)}$ is module-finite over $R_{i(j)}$ by the cover hypothesis and [F3]. A finite $R_{i(j)}$-module generating list tensors to a finite $C_j$-module generating list, so the coordinate algebra of $f^{-1}(W_j)$ is finite over $C_j$.

The same open restriction [F11], now over $U$, and the affine tensor formula [F10] identify the coordinate module of $f^{-1}(W_j)$ with $B{\otimes }_R{C}_j$. Flip the factors by [F18], then apply [F17] to $C_j{\otimes }_{R}B$ to identify this with the localization of the $R$-module $B$ at powers of $h_j$. Since the coordinate algebra in step 4.1 is finite over $C_j$, each such localized module $B_{h_j}$ is finitely generated over $R_{h_j}$.

For each of the finitely many $j$, choose a finite $R_{h_j}$-module generating list for $B_{h_j}$. Each generator is a fraction with numerator in $B$ and denominator a power of $h_j$; because that denominator is a unit after localization, its numerator can replace it in the generating list. Let $N\subseteq B$ be the $R$-submodule generated by all these finitely many numerators. Only finitely many lists are selected, which follows by induction on the finite index set and uses no AC. Then $N$ is finitely generated by [F13], and $N_{h_j}=B_{h_j}$ for every $j$.

Fix $b\in B$. Since $N_{h_j}=B_{h_j}$, for each $j$ there are $y_j\in N$ and $n_j\ge 0$ such that $b\mathrm{/}1=y_j\mathrm{/}{h}_j^{n_j}$ in $B_{h_j}$. Multiplying this equality by the unit $h_j^{n_j}$ in the localization [F16] shows $(h_j^{n_j}b-y_j)\mathrm{/}1=0$. By [F15], some power $h_j^{m_j}$ kills $h_j^{n_j}b-y_j$. These witnesses are selected for only finitely many $j$, so finite induction suffices and no AC is used. A positive power $h_j^{k_j}$ then sends $b$ into $N$ (if the resulting exponent is zero, increase it to one). Primeness gives $D(h_j^{k_j})=D(h_j)$, so these distinguished opens still cover $U$ [F6].

By [F12], the finite family $h_j^{k_j}$ generates the unit ideal of $R$. By [F19], write $1={\sum }_j{c}_j{h}_j^{k_j}$ with $c_j\in R$. For the arbitrary $b$ from step 7.1, each $h_j^{k_j}b$ lies in $N$, so $b={\sum }_j{c}_j{h}_j^{k_j}b\in N$. Thus $B=N$ is a finite $R$-module. This is the second AC use: [F12] supplies the unit-ideal relation from the principal cover.

Since $U$ was an arbitrary affine open, step 8.1 gives an affine inverse image with module-finite coordinate algebra over every such $U$; [F1] then shows $f$ is finite. For $h=0$ the localization is the zero module and $D(h)=\mathrm{\varnothing }$; for $h=1$ the localization is the whole module. If $U$ or an inverse-image chart is empty, its affine ring is zero and the zero module is generated by the empty list. No injectivity, flatness, reducedness, or finite-type assumption is used. The forward implication in step 1.1 remains choice-free, while the reverse implication assumes AC exactly as stated.