let n be Element of NAT ; :: thesis: for z being complex number holds
( (z ExpSeq ) . (n + 1) = (((z ExpSeq ) . n) * z) / ((n + 1) + (0 * <i> )) & (z ExpSeq ) . 0 = 1 & |.((z ExpSeq ) . n).| = (|.z.| rExpSeq ) . n )
let z be complex number ; :: thesis: ( (z ExpSeq ) . (n + 1) = (((z ExpSeq ) . n) * z) / ((n + 1) + (0 * <i> )) & (z ExpSeq ) . 0 = 1 & |.((z ExpSeq ) . n).| = (|.z.| rExpSeq ) . n )

A1: now

let n be Element of NAT ; :: thesis: (z ExpSeq ) . (n + 1) = (((z ExpSeq ) . n) * z) / ((n + 1) + (0 * <i> ))
thus (z ExpSeq ) . (n + 1) = (z |^ (n + 1)) / ((n + 1) !c ) by Def8
.= (((z GeoSeq ) . n) * z) / ((n + 1) !c ) by COMSEQ_3:def 1
.= ((z |^ n) * z) / ((n !c ) * ((n + 1) + (0 * <i> ))) by Th1
.= ((z |^ n) / (n !c )) * (z / ((n + 1) + (0 * <i> ))) by XCMPLX_1:77
.= (((z |^ n) / (n !c )) * z) / ((n + 1) + (0 * <i> ))
.= (((z ExpSeq ) . n) * z) / ((n + 1) + (0 * <i> )) by Def8 ; :: thesis: verum

end;

A2: (z ExpSeq ) . 0 = (z |^ 0 ) / (0 !c ) by Def8
.= 1 by Th1, COMSEQ_3:def 1 ;
defpred S₁[ Element of NAT ] means |.((z ExpSeq ) . $1).| = (|.z.| rExpSeq ) . $1;
(|.z.| rExpSeq ) . 0 = (|.z.| |^ 0 ) / (0 ! ) by Def9
.= 1 / (Prod_real_n . 0 ) by NEWTON:9
.= 1 / 1 by Def5
.= 1 ;
then A4: S₁[ 0 ] by A2, COMPLEX1:134;

A5: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: S₁[n] ; :: thesis: S₁[n + 1]
A7: |.((n + 1) + (0 * <i> )).| = n + 1 by ABSVALUE:def 1;
|.((z ExpSeq ) . (n + 1)).| = |.((((z ExpSeq ) . n) * z) / ((n + 1) + (0 * <i> ))).| by A1
.= |.(((z ExpSeq ) . n) * z).| / |.((n + 1) + (0 * <i> )).| by COMPLEX1:153
.= (((|.z.| rExpSeq ) . n) * |.z.|) / |.((n + 1) + (0 * <i> )).| by A6, COMPLEX1:151
.= (((|.z.| |^ n) / (n ! )) * |.z.|) / |.((n + 1) + (0 * <i> )).| by Def9
.= ((|.z.| |^ n) * |.z.|) / ((n ! ) * |.((n + 1) + (0 * <i> )).|) by XCMPLX_1:84
.= ((|.z.| |^ n) * |.z.|) / ((n + 1) ! ) by A7, NEWTON:21
.= (|.z.| |^ (n + 1)) / ((n + 1) ! ) by NEWTON:11
.= (|.z.| rExpSeq ) . (n + 1) by Def9 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A5);
hence ( (z ExpSeq ) . (n + 1) = (((z ExpSeq ) . n) * z) / ((n + 1) + (0 * <i> )) & (z ExpSeq ) . 0 = 1 & |.((z ExpSeq ) . n).| = (|.z.| rExpSeq ) . n ) by A1, A2; :: thesis: verum