Proof. sketch [1801A]

    1. Let $S \subseteq \overline{\mathbb{F}}_{p}$ be the set of roots of $x^{p^{n}} - x$. We first show that $S$ is a subfield of $\overline{\mathbb{F}}_{p}$, then we show that $\lvert S \rvert = p^{n} = \deg (x^{p^{n}} - x)$, this suffices to show that $x^{p^{n}} - x$ is separable.

      First, $0 \in S$. Given $\alpha, \beta \in S$, we have $(\alpha - \beta)^{p^{n}} - (\alpha - \beta) = \alpha^{p^{n}} - \beta^{p^{n}} - (\alpha - \beta) = 0$. Hence $\alpha - \beta \in S \implies (S, +)$ is a subgroup of $(\overline{\mathbb{F}}_{p}, +)$. Next, $(\alpha\beta)^{p^{n}} - \alpha\beta = \alpha^{p^{n}}\beta^{p^{n}} - \alpha\beta = 0 \implies \alpha\beta \in S$ and $(\alpha ^{-1})^{p^{n}} - \alpha ^{-1} = (\alpha^{p^{n}})^{-1} - \alpha ^{-1} = 0 \implies \alpha ^{-1} \in S$ shows that $S$ is a subfield of $\overline{\mathbb{F}}_{p}$. Moreover, $\mathbb{F}_{p^{n}} = \mathbb{F}_{p}[S] = S$. This is because any $\alpha \in \mathbb{F}_{p}$ satisfies $\alpha^{p^{n}} - \alpha = \alpha^{p^{n} - 1}\alpha - \alpha = 1 \cdot \alpha - \alpha = 0$ by Fermat’s little theorem. Hence $\alpha \in S$ $\implies$ $\mathbb{F}_{p}[S] = S$.

      Now since $(x^{p^{n}} - x)' = p^{n}x^{p^{n} - 1} - 1 = -1$, we have $\gcd(x^{p^{n}} - x, (x^{p^{n}} - x)') = 1$. By Proposition 1704, $x^{p^{n}} - x$ is separable over $\mathbb{F}_{p}$, hence $\lvert S \rvert = p^{n}$.

      Then we prove the uniqueness of $\mathbb{F}_{p^{n}}$. Suppose that $F$ is a subfield of $\overline{\mathbb{F}}_{p}$ with $\lvert F \rvert = p^{n}$. Then the multiplicative group $F^{\times}$ is abelian of order $p^{n} - 1$. By Lagrange’s Theorem, we know that $\alpha^{p^{n} - 1} = 1$ for all $\alpha \in F^{\times}$. Hence every element in $F$ is a root of $x^{p^{n}} - x$, hence $F \subseteq \mathbb{F}_{p^{n}}$. Since they have the same cardinality, $F = \mathbb{F}_{p^{n}}$.

    2. Let $F_{0}$ be $F$’s prime field. By the definition of $[F : F_{0}]$, which is $\dim_{F_{0}} F$, we have $\lvert F \rvert = \lvert F_{0} \rvert^{[F:F_{0}]}$. Hence $\lvert F_{0} \rvert$ is a prime that divides $p^{n}$ $\implies$ $\lvert F_{0} \rvert = p \implies F_{0} \cong \mathbb{F}_{p}$. Let $\varphi : F_{0} \to \overline{\mathbb{F}}_{p}$ be defined by $F_{0} \xrightarrow{\cong} \mathbb{F}_{p} \hookrightarrow \overline{\mathbb{F}}_{p}$. By [Proposition 1603], $\varphi$ extends to a field embedding $\psi : F \to \overline{\mathbb{F}}_{p}$. Then $\mathrm{Im}\psi \cong F$ is a subfield of $\overline{\mathbb{F}}_{p}$ and $\lvert \mathrm{Im}\psi \rvert = \lvert F \rvert = p^{n}$. By (1), we know that $\mathrm{Im}\psi = \mathbb{F}_{p^{n}}$. Therefore, $F \cong \mathbb{F}_{p^{n}}$.