let p be Prime; :: thesis: for n being non zero Nat
for F being GaloisField of p |^ n holds PrimeField F = Z/ p
let n be non zero Nat; :: thesis: for F being GaloisField of p |^ n holds PrimeField F = Z/ p
let F be GaloisField of p |^ n; :: thesis: PrimeField F = Z/ p
A: Z/ p is strict Subfield of F by defGal;
for E being strict Subfield of Z/ p holds E = Z/ p by RING_3:109;
hence PrimeField F = Z/ p by A, RING_3:92; :: thesis: verum