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) );

A1: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: 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 A2, COMPLFLD:90
.= (power F_Complex) . ((z *'),(k + 1)) by GROUP_1:def 8 ;
hence S₁[k + 1] ; :: thesis: verum

end;

((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 A3: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A1);
then ex j being Element of NAT st
( j = k & ((power F_Complex) . (z,j)) *' = (power F_Complex) . ((z *'),j) ) ;
hence ((power F_Complex) . (z,k)) *' = (power F_Complex) . ((z *'),k) ; :: thesis: verum