We proceed by induction on \([L: F]\text{.}\) In the base case, \([L: F]=1\text{,}\) and thus \(L=F\text{,}\) so \(\operatorname{Aut}(L / F)\) is the trivial group, and both statements hold.
Now let \(n \geqslant 1\) and suppose that \(|\operatorname{Aut}(L / F)| \leqslant[L: F]\) holds for all \(L\) and \(F\) such that \([L: F]<n\text{.}\) Let \([L: F]=n\text{.}\) Pick \(\alpha \in L \backslash F\) and let \(m=m_{\alpha, F}\text{,}\) and consider \(F(\alpha) / F\text{.}\)
Note that \(H=\operatorname{Aut}(L / F(\alpha))\) is a proper subgroup of \(G=\operatorname{Aut}(L / F)\text{.}\) By induction, we have \(|H| \leqslant[L: F(\alpha)]\text{.}\) We claim that it suffices to prove \([G: H] \leqslant[F(\alpha): F]\text{.}\) Indeed, using the Degree Formula and the fact that \(|G|=|H| \cdot[G: H]\text{,}\) if \([G: H] \leqslant[F(\alpha): F]\) then
\begin{equation*}
|G|=|H| \cdot[G: H] \leqslant[L: F(\alpha)][F(\alpha): F]=[L: F].
\end{equation*}
To show that \([G: H] \leqslant[F(\alpha): F]\text{,}\) consider the function
\begin{equation*}
\begin{gathered}
G / H=\{\text { cosets of } H \text { in } G\} \stackrel{\Psi}{\longrightarrow}\{\text { roots of } m \text { in } L\} \\
g H \longmapsto g(\alpha) .
\end{gathered}
\end{equation*}
By
Lemma 17.5, for any
\(g \in G\) the element
\(g(\alpha)\) is also a root of
\(m\text{.}\) For any
\(h \in H\text{,}\) we have
\begin{equation*}
g h(\alpha)=g(h(\alpha))=g(\alpha).
\end{equation*}
Thus \(\Psi\) is well-defined. Moreover, for any \(g_{1}, g_{2} \in G\) we have
\begin{equation*}
\Psi\left(g_{1} H\right)=\Psi\left(g_{2} H\right) \Longleftrightarrow g_{1}(\alpha)=g_{2}(\alpha) \Longleftrightarrow g_{2}^{-1} g_{1}(\alpha)=\alpha
\end{equation*}
which is equivalent to saying that \(g_{2}^{-1} g_{1}\) fixes \(F(\alpha)\text{,}\) and equivalently
\begin{equation*}
g_{2}^{-1} g_{1} \in H \Longleftrightarrow g_{1} H=g_{2} H.
\end{equation*}
This proves that the function \(\Psi\) is injective.
By Theorem [provisional cross-reference: cite] \(, \operatorname{deg}(m)=[F(\alpha): F]\text{.}\) Thus \(\Psi\) is an inclusion of \(G / H\) into a set with at most \([F(\alpha): F]\) many elements. Therefore,
\begin{equation*}
[G: H]=|G / H| \leqslant[F(\alpha): F].
\end{equation*}
Now suppose that \(f\) is separable, so that
\begin{equation*}
f=c \prod_{i=1}^{n}\left(x-\alpha_{i}\right) \in L[x].
\end{equation*}
with \(\alpha_{i} \neq \alpha_{j}\) for \(i \neq j\) and \(L=F\left(\alpha_{1}, \ldots, \alpha_{n}\right)\text{.}\)
Set \(\alpha=\alpha_{1}\) and let \(m\) be the irreducible factor of \(f\) that has \(\alpha\) as a root. Notice \(m=m_{\alpha, F}\text{.}\) As before, we consider \(F(\alpha)\) and set \(H=\operatorname{Aut}(L / F(\alpha)) \leq \operatorname{Aut}(L / F)=G\text{.}\) Note that \(L\) is also the splitting field of
\begin{equation*}
g=\prod_{i=2}^{n}\left(x-\alpha_{i}\right) \in F(\alpha)[x]
\end{equation*}
over \(F(\alpha)\text{,}\) and \(g\) is also separable. By induction \(|H|=[L: F(\alpha)]\text{,}\) and it remains to show that
\begin{equation*}
[G: H]=[F(\alpha): F]=\operatorname{deg}(m).
\end{equation*}
Since
\(f\) is separable, so is
\(m\text{,}\) so
\(\operatorname{deg}(m)\) is exactly the number of distinct roots of
\(m\text{.}\) Showing that
\([G: H]=\operatorname{deg}(m)\) amounts to the assertion that the injective map
\(\Psi\) is also surjective. This holds since
\(G\) acts transitively on the roots of
\(m\text{,}\) as shown in
Theorem 17.6.
