Proper birational normal curves agree off finitely many points

By [F1] the morphism $f$ is of finite type, hence locally of finite type by [F2]; since $f$ is birational in the sense of [F4] and $X,Y$ are integral finite-type $k$-schemes of dimension $1$, the principal-open result [F5] applies. It provides nonempty affine open subschemes $U=\mathrm{Spec}A\subseteq X$ and $V=\mathrm{Spec}B\subseteq Y$ with $f(U)\subseteq V$, the induced ring map $\phi :B\to A$, an element $\sigma \in B\setminus \{0\}$, and the conclusion that, with $U_0:=D(\phi (\sigma ))=f^{-1}(D(\sigma ))\cap U,V_0:=D(\sigma ),$ the restriction $f{\mathrm{\mid }}_{U_0}:U_0\to V_0$ is an isomorphism.

By [F7] the rings $A$ and $B$ are domains, so $\phi (\sigma )\mathrm{\ne }0$ in $A$ and $\sigma \mathrm{\ne }0$ in $B$; hence $(0)\in D(\phi (\sigma ))$ and $(0)\in D(\sigma )$ by [F8], which means that $U_0$ contains the generic point ${\eta }_X$ of $X$ and $V_0$ contains the generic point ${\eta }_Y$ of $Y$. Consequently $X\setminus U_0$ and $Y\setminus V_0$ are proper closed subsets of the curves $X$ and $Y$, so by [F6] both are finite sets of closed points of $X$, respectively $Y$.

Put $F:=f(X\setminus U_0)\cup (Y\setminus V_0)\subseteq Y$. This is a finite set: it is the union of the finite set $Y\setminus V_0$ with the image of the finite set $X\setminus U_0$. Every point of $F$ is a closed point of $Y$: points of $Y\setminus V_0$ are closed by step 1.2, and for $z\in X\setminus U_0$ the singleton $\{z\}$ is closed in $X$ by step 1.2, so its image under the closed map $f$ of [F3] is closed in $Y$; that image is $\{f(z)\}$, so $f(z)$ is a closed point of $Y$.

Let $y\in Y\setminus F$. Then $y\in V_0$, because $F$ contains the complement $Y\setminus V_0$, and $y\mathrm{\notin }f(X\setminus U_0)$. If $x\in X$ satisfies $f(x)=y$, then $x\mathrm{\notin }X\setminus U_0$ and therefore $x\in U_0$; hence $f^{-1}(Y\setminus F)\subseteq U_0\mathrm{.}$ Since $f(U_0)=V_0$ and $Y\setminus F\subseteq V_0$, the scheme $f^{-1}(Y\setminus F)$ is the inverse image under the isomorphism $f{\mathrm{\mid }}_{U_0}:U_0\to V_0$ of the open subscheme $Y\setminus F$ of $V_0$ (Open immersions of schemes [F9]), so the restriction of $f{\mathrm{\mid }}_{U_0}$ to it is an isomorphism $f^{-1}(Y\setminus F)\to Y\setminus F$.

Steps 2.1 and 3.1 exhibit the finite set $F$ of closed points of $Y$ whose removal makes $f$ an isomorphism, which is the claim. The normality hypothesis of [F10] and [F11] is not used in the argument: the chart computation of [F5] only needs $Y$ reduced, which integrality provides, and normality is a stronger hypothesis than the statement requires. The Axiom of Choice [F12] is used exactly through the curve lemma [F6] at step 1.2, whose proof assumes it; the remaining steps select nothing from an infinite family. If $F=\mathrm{\varnothing }$ the conclusion says that $f$ is already an isomorphism, and the argument still applies because the displayed sets may be empty. ∎