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