theorem Th30: :: EC_PF_1:30
for p being Prime ex g being Element of (GF p) st
for a being Element of (GF p) st a <> 0. (GF p) holds
ex n being Nat st a = g |^ n