now :: thesis: ( z <> 0c implies ( ( for n being Nat holds S₁[n] ) & z ExpSeq is absolutely_summable ) )

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

proof

let n be 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 Th3;
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₁( Nat) -> Element of REAL = (|.(z ExpSeq).| . (z + 1)) / (|.(z ExpSeq).| . z);
thus A6: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3); :: thesis: z ExpSeq is absolutely_summable
ex rseq being Real_Sequence st
for n being Nat holds rseq . n = H₁(n) from SEQ_1:sch 1();
then consider rseq being Real_Sequence such that
A7: for n being Nat holds rseq . n = (|.(z ExpSeq).| . (n + 1)) / (|.(z ExpSeq).| . n) ;

now :: thesis: for n being Nat holds rseq . n = |.z.| / (n + 1)

let n be 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:67
.= |.(((((z ExpSeq) . n) * z) / ((n + 1) + (0 * <i>))) / ((z ExpSeq) . n)).| by Th3
.= |.((((z ExpSeq) . n) * (z / ((n + 1) + (0 * <i>)))) / ((z ExpSeq) . n)).|
.= |.(z / ((n + 1) + (0 * <i>))).| by A6, XCMPLX_1:89
.= |.z.| / |.(n + 1).| by COMPLEX1:67
.= |.z.| / (n + 1) by ABSVALUE:def 1 ; :: thesis: verum

end;

then ( rseq is convergent & lim rseq < 1 ) by SEQ_4:31;
hence z ExpSeq is absolutely_summable by A6, A7, COMSEQ_3:75; :: thesis: verum

end;

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