let F be finite Field; :: thesis: F is PrimeField F -normal PrimeField F -separable FieldExtension of PrimeField F
consider p being Prime, n being non zero Nat such that
A: ( Char F = p & order F = p |^ n ) by finex2;
reconsider E = F as SplittingField of X^ ((p |^ n),(PrimeField F)) by A, split;
E is PrimeField F -normal FieldExtension of PrimeField F ;
hence F is PrimeField F -normal PrimeField F -separable FieldExtension of PrimeField F ; :: thesis: verum