Every finite field has order $p^n$ for a unique prime characteristic $p$ and positive integer $n$

The characteristic cannot be zero, because the distinct integer multiples of $1_F$ would give infinitely many elements. Hence it is a unique prime $p$, and [L2] identifies the prime subfield with ${\mathbb{F}}_p$.

Enumerate the finite set $F$ as $a_1,\dots ,a_N$. Starting with the empty list, inspect these elements in order and append $a_i$ exactly when it is outside the span of the previously appended elements. Inductively the retained list is linearly independent, and its span after step $i$ contains $a_1,\dots ,a_i$: if $a_i$ is not appended it already lies in that span. After the finitely many steps the list spans $F$, so it is a finite basis over ${\mathbb{F}}_p$. Its length $n$ is positive because $1_F\mathrm{\ne }0$, and [L3] identifies $n$ with $[F:{\mathbb{F}}_p]$. This finite construction uses no Axiom of Choice.

By [L5], taking coordinates is a bijection from $F$ to the functions from an $n$-element basis index set to ${\mathbb{F}}_p$. Thus [L6] gives $\mathrm{\mid }F\mathrm{\mid }=p^n$.

Steps 1.1 and 1.2 exhibit the pair $(p,n)$ with $p=\mathrm{char}F$ and $n=[F:{\mathbb{F}}_p]$. For uniqueness, suppose also $\mathrm{\mid }F\mathrm{\mid }={\mathrm{\ell }}^m$ with $\mathrm{\ell }$ prime and $m\ge 1$. Then $p$ divides ${\mathrm{\ell }}^m$, so [L7] gives $p\mid \mathrm{\ell }$, and primality of $\mathrm{\ell }$ forces $p=\mathrm{\ell }$. Now $p^n=p^m$ with $p\ge 2$ forces $n=m$, since $n<m$ would give $1=p^{m-n}\ge p\ge 2$ and symmetrically for $m<n$.