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 S1[ Nat] means ex j being Element of NAT st
( j = $1 & ((power F_Complex) . (z,j)) *' = (power F_Complex) . ((z *'),j) );
A1: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
assume A2: S1[k] ; :: thesis: S1[k + 1]
((power F_Complex) . (z,(k + 1))) *' = (((power F_Complex) . (z,kk)) * z) *' by GROUP_1:def 7
.= ((power F_Complex) . ((z *'),kk)) * (z *') by A2, COMPLFLD:54
.= (power F_Complex) . ((z *'),(k + 1)) by GROUP_1:def 7 ;
hence S1[k + 1] ; :: thesis: verum
end;
((power F_Complex) . (z,0)) *' = (1_ F_Complex) *' by GROUP_1:def 7
.= 1_ F_Complex by Lm2, COMPLEX1:38
.= (power F_Complex) . ((z *'),0) by GROUP_1:def 7 ;
then A3: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(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