now

assume A1: 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 ;
A2: S₁[ 0 ] by Th4;
A3: 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 A4: (z ExpSeq ) . n <> 0c ; :: thesis: S₁[n + 1]
thus (z ExpSeq ) . (n + 1) <> 0c :: thesis: verum

proof

assume (z ExpSeq ) . (n + 1) = 0c ; :: thesis: contradiction
then A5: (((z ExpSeq ) . n) * z) / ((n + 1) + (0 * <i> )) = 0c by Th4;
0c = 0c / z
.= (((z ExpSeq ) . n) * z) / z by A5, XCMPLX_1:50
.= ((z ExpSeq ) . n) * (z / z)
.= ((z ExpSeq ) . n) * 1 by A1, XCMPLX_1:60
.= (z ExpSeq ) . n ;
hence contradiction by A4; :: thesis: verum

end;

end;

deffunc H₁( Element of NAT ) -> Element of REAL = (|.(z ExpSeq ).| . (z + 1)) / (|.(z ExpSeq ).| . z);
thus A6: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A3); :: thesis: z ExpSeq is absolutely_summable
ex rseq being Real_Sequence st
for n being Element of NAT holds rseq . n = H₁(n) from SEQ_1:sch 1();
then consider rseq being Real_Sequence such that
A7: for n being Element of NAT holds rseq . n = (|.(z ExpSeq ).| . (n + 1)) / (|.(z ExpSeq ).| . n) ;
( rseq is convergent & lim rseq < 1 )

proof

now

let n be Element of NAT ; :: thesis: rseq . n = |.z.| / (n + 1)
thus rseq . n = (|.(z ExpSeq ).| . (n + 1)) / (|.(z ExpSeq ).| . n) by A7
.= |.((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 A6, XCMPLX_1:90
.= |.z.| / (abs (n + 1)) by COMPLEX1:153
.= |.z.| / (n + 1) by ABSVALUE:def 1 ; :: thesis: verum

end;

hence ( rseq is convergent & lim rseq < 1 ) by SEQ_4:46; :: thesis: verum

end;

hence z ExpSeq is absolutely_summable by A6, A7, COMSEQ_3:76; :: thesis: verum

end;

hence z ExpSeq is absolutely_summable by Th10; :: thesis: verum