let n be Nat; :: thesis: for z being Complex 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; :: 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 :: thesis: for n being Nat holds (z ExpSeq) . (n + 1) = (((z ExpSeq) . n) * z) / ((n + 1) + (0 * <i>))

let n be Nat; :: thesis: (z ExpSeq) . (n + 1) = (((z ExpSeq) . n) * z) / ((n + 1) + (0 * <i>))
thus (z ExpSeq) . (n + 1) = (z |^ (n + 1)) / ((n + 1) !) by Def4
.= (((z GeoSeq) . n) * z) / ((n + 1) !) by COMSEQ_3:def 1
.= ((z |^ n) * z) / ((n !) * ((n + 1) + (0 * <i>))) by Th1
.= ((z |^ n) / (n !)) * (z / ((n + 1) + (0 * <i>))) by XCMPLX_1:76
.= (((z |^ n) / (n !)) * z) / ((n + 1) + (0 * <i>))
.= (((z ExpSeq) . n) * z) / ((n + 1) + (0 * <i>)) by Def4 ; :: thesis: verum

end;

A2: (z ExpSeq) . 0 = (z |^ 0) / (0 !) by Def4
.= 1 by Th1, COMSEQ_3:def 1 ;
defpred S₁[ Nat] means |.((z ExpSeq) . $1).| = (|.z.| rExpSeq) . $1;
(|.z.| rExpSeq) . 0 = (|.z.| |^ 0) / (0 !) by Def5
.= 1 / (Prod_real_n . 0) by NEWTON:4
.= 1 / 1 by Def2
.= 1 ;
then A3: S₁[ 0 ] by A2, COMPLEX1:48;

A4: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
A6: |.((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:67
.= (((|.z.| rExpSeq) . n) * |.z.|) / |.((n + 1) + (0 * <i>)).| by A5, COMPLEX1:65
.= (((|.z.| |^ n) / (n !)) * |.z.|) / |.((n + 1) + (0 * <i>)).| by Def5
.= ((|.z.| |^ n) * |.z.|) / ((n !) * |.((n + 1) + (0 * <i>)).|) by XCMPLX_1:83
.= ((|.z.| |^ n) * |.z.|) / ((n + 1) !) by A6, NEWTON:15
.= (|.z.| |^ (n + 1)) / ((n + 1) !) by NEWTON:6
.= (|.z.| rExpSeq) . (n + 1) by Def5 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
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