theorem Th14: :: EC_PF_1:14

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