let z be Element of F_Complex; for k being Element of NAT holds ((power F_Complex) . (z,k)) *' = (power F_Complex) . ((z *'),k)
let k be Element of NAT ; ((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 for k being Nat st S1[k] holds
S1[k + 1]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)
; verum