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$.

The finite set $F$ spans itself over ${\mathbb{F}}_p$, so [L4] supplies a finite basis. Its size $n$ is positive because $F$ is not the zero vector space.

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$.