theorem T5: :: FIELD_16:27

for p being Prime
for n being non zero Nat
for F being Field st card F = p |^ n holds
Char F = p