A1: now

assume A2: z <> 0c ; :: thesis: ( ( for n being Element of NAT holds S₁[n] ) & z ExpSeq is absolutely_summable )
defpred S₁[ set ] means (z ExpSeq ) . z <> 0c ;
A3: S₁[ 0 ] by Th4;
A4: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: (z ExpSeq ) . n <> 0c ; :: thesis: S₁[n + 1]
thus (z ExpSeq ) . (n + 1) <> 0c :: thesis: verum

proof

assume A6: (z ExpSeq ) . (n + 1) = 0c ; :: thesis: contradiction
A7: (((z ExpSeq ) . n) * z) / ((n + 1) + (0 * <i> )) = 0c by A6, Th4;
A8: 0c = 0c / z
.= (((z ExpSeq ) . n) * z) / z by A7, XCMPLX_1:50
.= ((z ExpSeq ) . n) * (z / z)
.= ((z ExpSeq ) . n) * 1 by A2, XCMPLX_1:60
.= (z ExpSeq ) . n ;
thus contradiction by A5, A8; :: thesis: verum

end;

end;

deffunc H₁( Element of NAT ) -> Element of REAL = (|.(z ExpSeq ).| . (z + 1)) / (|.(z ExpSeq ).| . z);
thus A9: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A4); :: thesis: z ExpSeq is absolutely_summable
A10: ex rseq being Real_Sequence st
for n being Element of NAT holds rseq . n = H₁(n) from SEQ_1:sch 1();
consider rseq being Real_Sequence such that
A11: for n being Element of NAT holds rseq . n = (|.(z ExpSeq ).| . (n + 1)) / (|.(z ExpSeq ).| . n) by A10;

A12: now

let n be Element of NAT ; :: thesis: rseq . n = |.z.| / (n + 1)
thus rseq . n = (|.(z ExpSeq ).| . (n + 1)) / (|.(z ExpSeq ).| . n) by A11
.= |.((z ExpSeq ) . (n + 1)).| / (|.(z ExpSeq ).| . n) by VALUED_1:18
.= |.((z ExpSeq ) . (n + 1)).| / |.((z ExpSeq ) . n).| by VALUED_1:18
.= |.(((z ExpSeq ) . (n + 1)) / ((z ExpSeq ) . n)).| by COMPLEX1:153
.= |.(((((z ExpSeq ) . n) * z) / ((n + 1) + (0 * <i> ))) / ((z ExpSeq ) . n)).| by Th4
.= |.((((z ExpSeq ) . n) * (z / ((n + 1) + (0 * <i> )))) / ((z ExpSeq ) . n)).|
.= |.(z / ((n + 1) + (0 * <i> ))).| by A9, XCMPLX_1:90
.= |.z.| / (abs (n + 1)) by COMPLEX1:153
.= |.z.| / (n + 1) by ABSVALUE:def 1 ; :: thesis: verum

end;

A13: ( rseq is convergent & lim rseq < 1 ) by A12, SEQ_4:46;
thus z ExpSeq is absolutely_summable by A9, A11, A13, COMSEQ_3:76; :: thesis: verum

end;

thus z ExpSeq is absolutely_summable by A1, Th10; :: thesis: verum