theorem Th16: :: NAT_6:16

for p being Prime
for x, y being Element of (Z/Z* p)
for i, j being Integer st x = i & y = j holds
x * y = (i * j) mod p