let p be Prime; :: thesis: 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); :: thesis: 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); :: thesis: ( z = y implies for n being Element of NAT holds (power (Z/Z* p)) . (z,n) = (power (INT.Ring p)) . (y,n) )
defpred S₁[ Nat] means (power (Z/Z* p)) . (z,$1) = (power (INT.Ring p)) . (y,$1);
assume A1: z = y ; :: thesis: for n being Element of NAT holds (power (Z/Z* p)) . (z,n) = (power (INT.Ring p)) . (y,n)

A2: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
(power (Z/Z* p)) . (z,(k + 1)) = ((power (Z/Z* p)) . (z,k)) * z by GROUP_1:def 7
.= ((power (INT.Ring p)) . (y,k)) * y by A1, A3, Lm12
.= (power (INT.Ring p)) . (y,(k + 1)) by GROUP_1:def 7 ;
hence S₁[k + 1] ; :: thesis: verum

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: S₁[ 0 ] ;
for k being Nat holds S₁[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) ; :: thesis: verum