A nonconstant rational function defines a finite map to the projective line

By [F10], every point other than the generic point of $C$ is closed. The local rings at those points are discrete valuation rings by [F3], the generic local ring is $K$, and these rings are integrally closed by [F11]. Thus $C$ is normal and [F1] applies.

If $f$ were algebraic over $k$, [F1] would make it a global unit; by [F2] that unit lies in $k^{\times }$, contradicting nonconstancy. Thus $f$ is transcendental. Here nonconstant means $f\mathrm{\notin }k$: if an algebraic element of $K$ lies outside $k$, the same supplier and $H^0(C,{\mathcal{O}}_C)=k$ force it into $k$.

The transcendental case of [F1] gives a finite locally free map ${\phi }_f:C\to {\mathbb{P}}_k^1$ of degree $d=[K:k(f)]$, with $t\mapsto f$ on $U_0$ and $s\mapsto f^{-1}$ on $U_1$ by [F4]. The generic point maps to the generic point.

Let any $g\in K^{\times }$ have no poles. Then ${\mathrm{ord}}_x(g)\ge 0$ gives $g\in {\mathcal{O}}_{C,x}$ at every closed point by [F3], and it belongs to the generic stalk $K$. Each stalk membership has a local representative in ${\mathcal{O}}_C$ by [F9]; all representatives map to the same $g$ in the constant meromorphic sheaf, so injectivity makes them agree on overlaps and the sheaf axiom glues them to a global section.

By [F2], the global section from the preceding argument lies in $H^0(C,{\mathcal{O}}_C)=k$. Since $g\mathrm{\ne }0$, it is in $k^{\times }$, hence algebraic over $k$ and a global unit.

Write ${\phi }_f^{-1}(U_0)=\mathrm{Spec}{B}_0$, with $k[t]\to B_0$ sending $t$ to $f$ by [F1]. Base change to $0=\mathrm{Spec}(k[t]\mathrm{/}(t))$ gives the actual fibre $C_0=\mathrm{Spec}(B_0{\otimes }_{k[t]}k)=\mathrm{Spec}(B_0\mathrm{/}f{B}_0)$.

The generic point is not in $C_0$ by [F1], so [F10] makes all its points closed. At a closed point $x$, ${\phi }_f(x)=0$ exactly when $f\in {\mathfrak{m}}_x$, or ${\mathrm{ord}}_x(f)>0$ by [F3]. Conversely, a positive order makes $f$ regular with zero residue and $f^{-1}\mathrm{\notin }{\mathcal{O}}_{C,x}$, so [F1] puts $x$ over $U_0$ with $t$-value $0$; on $U_0\setminus \{0\}$, $t$ and its pullback $f$ are units, while points outside $U_0$ map to $\mathrm{\infty }$. Thus these are exactly the zero-fibre points.

For each $x\in C_0$, [F6] gives ${\mathcal{O}}_{C_0,x}\cong {\mathcal{O}}_{C,x}\mathrm{/}(f)$. Writing $f=u{\pi }_x^m$ with $m={\mathrm{ord}}_x(f)>0$, this is ${\mathcal{O}}_{C,x}\mathrm{/}({\pi }_x^m)$ and has length $m$ by [F12].

On ${\phi }_f^{-1}(U_0)$ the fibre is cut out by $f$; on the open complement of its support it is empty and cut out by $1$. The germs of $f$ are nonzero in the local domains since they map to $f\mathrm{\ne }0$ in $K$, and $f$ is a unit on the overlap because it maps into $U_0\setminus \{0\}$. These compatible nonzerodivisor equations make the fibre an effective Cartier divisor by [F7]. Its coefficient at $x$ is the order $m$ of its local equation, and it has coefficient zero elsewhere; hence $C_0=(f{)}_0={\sum }_{{\mathrm{ord}}_x(f)>0}{\mathrm{ord}}_x(f)[x]$.

Write ${\phi }_f^{-1}(U_1)=\mathrm{Spec}{B}_1$, with $k[s]\to B_1$ sending $s$ to $f^{-1}$. Base change to $\mathrm{\infty }=\mathrm{Spec}(k[s]\mathrm{/}(s))$ gives $C_{\mathrm{\infty }}=\mathrm{Spec}(B_1{\otimes }_{k[s]}k)=\mathrm{Spec}(B_1\mathrm{/}{f}^{-1}{B}_1)$. Its points are closed by [F10] because the generic point maps to the generic point.

A closed point $x$ lies over $\mathrm{\infty }$ exactly when $f^{-1}\in {\mathfrak{m}}_x$, or ${\mathrm{ord}}_x(f)<0$; conversely, this negative order makes $f^{-1}$ regular with zero residue and $f\mathrm{\notin }{\mathcal{O}}_{C,x}$, so [F1] places $x$ over $U_1$ with $s$-value zero. Away from $\mathrm{\infty }$ in $U_1$, $s$ and its pullback $f^{-1}$ are units; points outside $U_1$ map to $0$.

For each $x\in C_{\mathrm{\infty }}$, put $m=-{\mathrm{ord}}_x(f)>0$. The fibre-stalk quotient is ${\mathcal{O}}_{C,x}\mathrm{/}(f^{-1})={\mathcal{O}}_{C,x}\mathrm{/}({\pi }_x^m)$ up to a unit, so it has length $m$ by [F12].

The equations $f^{-1}$ on ${\phi }_f^{-1}(U_1)$ and $1$ off the fibre are compatible nonzerodivisors: the germs of $f^{-1}$ map to the nonzero element $f^{-1}$ in $K$, and it is a unit on the overlap mapping into $U_1\setminus \{\mathrm{\infty }\}$. By [F7] they define the effective Cartier fibre; its local Weil coefficient is $m=-{\mathrm{ord}}_x(f)$ and is zero elsewhere. Hence $C_{\mathrm{\infty }}=(f{)}_{\mathrm{\infty }}={\sum }_{{\mathrm{ord}}_x(f)<0}(-{\mathrm{ord}}_x(f))[x]$.

By [F5], the weighted residue-degree sums of these actual zero and pole fibres both equal $d=[K:k(f)]$. The divisor degree convention in [F8] therefore gives ${\mathrm{deg}}_k((f{)}_0)={\mathrm{deg}}_k((f{)}_{\mathrm{\infty }})=[K:k(f)]$.

The constructed morphism is finite locally free of degree $[K:k(f)]$, its actual scheme-theoretic zero and infinity fibres are the stated effective Cartier/Weil divisors with the displayed local multiplicities, and both have degree $[K:k(f)]$. The no-poles argument shows that every nonzero rational function with no poles is in $k^{\times }$, hence algebraic and a global unit. The Axiom of Choice enters through [F1], [F2], [F3] and [F5].