for i being Integer
for p being Prime holds i mod p is Element of (GF p)