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 )
assume A1: z = y ; :: thesis: 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;
A2: S₁[ 0 ]

proof

thus (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 ; :: thesis: verum

end;

A3: now

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

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A3);
hence for n being Element of NAT holds (power (Z/Z* p)) . z,n = (power (INT.Ring p)) . y,n ; :: thesis: verum