theorem Th34: :: EC_PF_1:34

for p being Prime
for a being Element of (GF p) holds
( a = 0 iff Lege_p a = 0 ) by Def5;