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