defpred S1[ set ] means (Partial_Sums |.(0c ExpSeq).|) . $1 = jj;
(Partial_Sums |.(0c ExpSeq).|) . 0 = |.(0c ExpSeq).| . 0 by SERIES_1:def 1
.= |.((0c ExpSeq) . 0).| by VALUED_1:18
.= 1 by Th3, COMPLEX1:48 ;
then A1: S1[ 0 ] ;
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A3: (Partial_Sums |.(0c ExpSeq).|) . n = jj ; :: thesis: S1[n + 1]
thus (Partial_Sums |.(0c ExpSeq).|) . (n + 1) = 1 + (|.(0c ExpSeq).| . (n + 1)) by A3, SERIES_1:def 1
.= 1 + |.((0c ExpSeq) . (n + 1)).| by VALUED_1:18
.= 1 + |.((((0c ExpSeq) . n) * 0c) / ((n + 1) + (0 * <i>))).| by Th3
.= jj by COMPLEX1:44 ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A1, A2);
 then Partial_Sums |.(0c ExpSeq).| is constant by VALUED_0:def 18;
then A4: |.(0c ExpSeq).| is summable by SERIES_1:def 2;
defpred S2[ set ] means (Partial_Sums (0c ExpSeq)) . $1 = 1;
(Partial_Sums (0c ExpSeq)) . 0 = (0c ExpSeq) . 0 by SERIES_1:def 1
.= 1 by Th3 ;
then A5: S2[ 0 ] ;
A6: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A7: (Partial_Sums (0c ExpSeq)) . n = 1 ; :: thesis: S2[n + 1]
thus (Partial_Sums (0c ExpSeq)) . (n + 1) = 1r + ((0c ExpSeq) . (n + 1)) by A7, SERIES_1:def 1
.= 1r + ((((0c ExpSeq) . n) * 0c) / ((n + 1) + (0 * <i>))) by Th3
.= 1 ; :: thesis: verum
end;
for n being Nat holds S2[n] from NAT_1:sch 2(A5, A6);
 hence ( 0c ExpSeq is absolutely_summable & Sum (0c ExpSeq) = 1r ) by A4, COMSEQ_2:10; :: thesis: verum