theorem PF: :: FIELD_16:70

for p being Prime
for n being non zero Nat
for F being GaloisField of p |^ n holds PrimeField F = Z/ p