for i, j being Integer
for p being Prime
for a, b being Element of (GF p) st a = i mod p & b = j mod p holds
a + b = (i + j) mod p