let z be Element of F_Complex ; :: thesis: for k being Element of NAT holds ((power F_Complex ) . z,k) *' = (power F_Complex ) . (z *' ),k
let k be Element of NAT ; :: thesis: ((power F_Complex ) . z,k) *' = (power F_Complex ) . (z *' ),k
defpred S₁[ Nat] means ex j being Element of NAT st
( j = $1 & ((power F_Complex ) . z,j) *' = (power F_Complex ) . (z *' ),j );
((power F_Complex ) . z,0 ) *' = (1_ F_Complex ) *' by GROUP_1:def 8
.= 1_ F_Complex by Lm2, Lm3
.= (power F_Complex ) . (z *' ),0 by GROUP_1:def 8 ;
then A1: S₁[ 0 ] ;

A2: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
((power F_Complex ) . z,(k + 1)) *' = (((power F_Complex ) . z,k) * z) *' by GROUP_1:def 8
.= ((power F_Complex ) . (z *' ),k) * (z *' ) by A3, COMPLFLD:90
.= (power F_Complex ) . (z *' ),(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(A1, A2);
then consider j being Element of NAT such that
A4: ( j = k & ((power F_Complex ) . z,j) *' = (power F_Complex ) . (z *' ),j ) ;
thus ((power F_Complex ) . z,k) *' = (power F_Complex ) . (z *' ),k by A4; :: thesis: verum