theorem Th17: :: NAT_6:17

for p being Prime
for x being Element of (Z/Z* p)
for i being Integer
for n being Nat st x = i holds
x |^ n = (i |^ n) mod p