theorem thX0: :: FIELD_16:28

for p being Prime
for n being non zero Nat
for F being Field st card F = p |^ n holds
for a being Element of F holds a |^ (p |^ n) = a