theorem Th25: :: EC_PF_1:25

for n being Nat
for p being Prime
for a being Element of (GF p) st a <> 0 holds
a |^ n <> 0