theorem Th28: :: INT_7:28

for p being Prime
for z being Element of (Z/Z* p)
for y being Element of (INT.Ring p) st z = y holds
for n being Element of NAT holds (power (Z/Z* p)) . (z,n) = (power (INT.Ring p)) . (y,n)