[step:Promote algebraic to finite using finite generation]
We show $\mathcal{O}_C(\eta) / \mathcal{O}_D(\eta)$ is finite.
By [Function Field is Finitely Generated](/theorems/2142), $\mathcal{O}_C(\eta)$ is a finitely generated field extension of $k$. Concretely, $\mathcal{O}_C(\eta) = k(\alpha_1, \ldots, \alpha_r)$ for some elements $\alpha_1, \ldots, \alpha_r \in \mathcal{O}_C(\eta)$. Since $k(t) \supset k$, this also gives
\begin{align*}
\mathcal{O}_C(\eta) = k(t)(\alpha_1, \ldots, \alpha_r),
\end{align*}
i.e. $\mathcal{O}_C(\eta)$ is finitely generated as a field extension of $k(t)$.
By Step 4, $\mathcal{O}_C(\eta) / k(t)$ is algebraic. Each generator $\alpha_i$ is therefore algebraic over $k(t)$, with some finite degree $d_i := [k(t)(\alpha_i) : k(t)]$. Building up the tower
\begin{align*}
k(t) \subset k(t)(\alpha_1) \subset k(t)(\alpha_1, \alpha_2) \subset \cdots \subset k(t)(\alpha_1, \ldots, \alpha_r) = \mathcal{O}_C(\eta),
\end{align*}
each successive extension is generated by a single algebraic element over the previous field, hence finite of degree at most $d_i$ (the degree may drop if $\alpha_i$ already lies in the previous field, but cannot exceed $d_i$). By the multiplicativity of degrees in towers,
\begin{align*}
[\mathcal{O}_C(\eta) : k(t)] \leq d_1 d_2 \cdots d_r < \infty.
\end{align*}
Now use the tower $k(t) \subset \mathcal{O}_D(\eta) \subset \mathcal{O}_C(\eta)$ from Step 4. Multiplicativity of degrees,
\begin{align*}
[\mathcal{O}_C(\eta) : k(t)] = [\mathcal{O}_C(\eta) : \mathcal{O}_D(\eta)] \cdot [\mathcal{O}_D(\eta) : k(t)],
\end{align*}
together with $[\mathcal{O}_C(\eta) : k(t)] < \infty$, forces both $[\mathcal{O}_C(\eta) : \mathcal{O}_D(\eta)]$ and $[\mathcal{O}_D(\eta) : k(t)]$ to be finite — both are positive divisors of a finite product. In particular,
\begin{align*}
[\mathcal{O}_C(\eta) : \mathcal{O}_D(\eta)] < \infty.
\end{align*}
A finite extension of fields is automatically algebraic (every element of a finite extension is algebraic, because $1, \alpha, \alpha^2, \ldots$ cannot all be linearly independent over a finite-dimensional vector space). This proves (2).
[/step]