theorem :: EC_PF_1:19

for i, j being Integer
for p being Prime
for a being Element of (GF p) st a = i mod p & (i * j) mod p = 1 holds
a " = j mod p