theorem Th16: :: NAT_6:16

for p being natural prime number
for x, y being Element of (Z/Z* p)
for i, j being integer number st x = i & y = j holds
x * y = (i * j) mod p