Descent of vanishing along a faithfully flat morphism

Let $s\in S$ be arbitrary. Since $f$ is surjective by [F1], the set $f^{-1}(s)$ is nonempty; the argument that follows is uniform in $s$ and produces no simultaneous choice over $S$.

Fix $x\in X$ with $f(x)=s$. By [F2], [F3] and [F4] the stalk of the pullback at $x$ is $(f^{\ast }\mathcal{F}{)}_x\cong {\mathcal{F}}_s{\otimes }_{{\mathcal{O}}_{S,s}}{\mathcal{O}}_{X,x}$.

Put $A={\mathcal{O}}_{S,s}$, $B={\mathcal{O}}_{X,x}$, and let $\mathfrak{m},\mathfrak{n}$ be their maximal ideals. The map $A\to B$ is local and $B$ is flat over $A$, because $f$ is flat at $x$. For any proper ideal $I\subset A$, [F5] gives $I\subseteq \mathfrak{m}$; locality gives $IB\subseteq \mathfrak{n}$, so $B\mathrm{/}IB\mathrm{\ne }0$. This uses the explicit localization at the fixed point $s$, with no maximal-ideal existence choice.

Suppose ${\mathcal{F}}_s\mathrm{\ne }0$ and fix $0\mathrm{\ne }v\in {\mathcal{F}}_s$. Its annihilator $I={\mathrm{Ann}}_A(v)$ is proper, and the cyclic submodule $Av\cong A\mathrm{/}I$ injects into ${\mathcal{F}}_s$. By [F6] and flatness in step 1.3, $B\mathrm{/}IB\cong (Av){\otimes }_{A}B$ injects into ${\mathcal{F}}_s{\otimes }_{A}B$. The source is nonzero by step 1.3, so $(f^{\ast }\mathcal{F}{)}_x\mathrm{\ne }0$ by step 1.2. Hence $f^{\ast }\mathcal{F}=0$ forces ${\mathcal{F}}_s=0$. Since $s$ was arbitrary and only one $x$ over that fixed $s$ was used, every stalk of $\mathcal{F}$ vanishes.

The zero morphism $0\to \mathcal{F}$ of ${\mathcal{O}}_S$-modules has stalk maps $0\to {\mathcal{F}}_s$ at every $s\in S$, which are isomorphisms because ${\mathcal{F}}_s=0$ by step 2.1. By [F7] the zero morphism is an isomorphism, that is, $\mathcal{F}=0$. Nothing in steps 1.1-2.1 used quasi-coherence of $\mathcal{F}$ or finiteness of $X$, and the only selection made is one point of one nonempty fibre at a time, so the proof is choice-free. [F7, step 2.1] $\mathrm{\square }$