theorem Th13: :: EC_PF_1:13

for p being Prime
for a being Element of (GF p) ex n1 being Nat st a = n1 mod p