let p be 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)
let z be 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)
let y be Element of (INT.Ring p); ( z = y implies for n being Element of NAT holds (power (Z/Z* p)) . (z,n) = (power (INT.Ring p)) . (y,n) )
defpred S1[ Nat] means (power (Z/Z* p)) . (z,$1) = (power (INT.Ring p)) . (y,$1);
assume A1:
z = y
; for n being Element of NAT holds (power (Z/Z* p)) . (z,n) = (power (INT.Ring p)) . (y,n)
A2:
now for k being Nat st S1[k] holds
S1[k + 1]end;
(power (Z/Z* p)) . (z,0) =
1_ (Z/Z* p)
by GROUP_1:def 7
.=
1_ (INT.Ring p)
by Th21
.=
(power (INT.Ring p)) . (y,0)
by GROUP_1:def 7
;
then A4:
S1[ 0 ]
;
for k being Nat holds S1[k]
from NAT_1:sch 2(A4, A2);
hence
for n being Element of NAT holds (power (Z/Z* p)) . (z,n) = (power (INT.Ring p)) . (y,n)
; verum