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

let k be Element of 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 8
.= ((power (INT.Ring p)) . y,k) * y by A1, A3, Lm12
.= (power (INT.Ring p)) . y,(k + 1) by GROUP_1:def 8 ;
hence S₁[k + 1] ; :: thesis: verum

end;

(power (Z/Z* p)) . z,0 = 1_ (Z/Z* p) by GROUP_1:def 8
.= 1_ (INT.Ring p) by Th21
.= (power (INT.Ring p)) . y,0 by GROUP_1:def 8 ;
then A4: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A2);
hence for n being Element of NAT holds (power (Z/Z* p)) . z,n = (power (INT.Ring p)) . y,n ; :: thesis: verum