let F be GaloisField of p |^ n; :: thesis: ( F is Z/ p -normal & F is Z/ p -separable )
PrimeField F = Z/ p by PF;
hence ( F is Z/ p -normal & F is Z/ p -separable ) by ThNS; :: thesis: verum