defpred S₁[ set ] means (Partial_Sums |.(0c ExpSeq ).|) . $1 = 1;
A1: (Partial_Sums |.(0c ExpSeq ).|) . 0 = |.(0c ExpSeq ).| . 0 by SERIES_1:def 1
.= |.((0c ExpSeq ) . 0 ).| by VALUED_1:18
.= 1 by Th4, COMPLEX1:134 ;
A2: S₁[ 0 ] by A1;
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: (Partial_Sums |.(0c ExpSeq ).|) . n = 1 ; :: thesis: S₁[n + 1]
A5: n in NAT by ORDINAL1:def 13;
thus (Partial_Sums |.(0c ExpSeq ).|) . (n + 1) = 1 + (|.(0c ExpSeq ).| . (n + 1)) by A4, A5, SERIES_1:def 1
.= 1 + |.((0c ExpSeq ) . (n + 1)).| by VALUED_1:18
.= 1 + |.((((0c ExpSeq ) . n) * 0c ) / ((n + 1) + (0 * <i> ))).| by A5, Th4
.= 1 by COMPLEX1:130 ; :: thesis: verum

end;

A6: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
A7: Partial_Sums |.(0c ExpSeq ).| is constant by A6, VALUED_0:def 18;
A8: |.(0c ExpSeq ).| is summable by A7, SERIES_1:def 2;
defpred S₂[ set ] means (Partial_Sums (0c ExpSeq )) . $1 = 1;
A9: (Partial_Sums (0c ExpSeq )) . 0 = (0c ExpSeq ) . 0 by COMSEQ_3:def 7
.= 1 by Th4 ;
A10: S₂[ 0 ] by A9;
A11: 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 A12: (Partial_Sums (0c ExpSeq )) . n = 1 ; :: thesis: S₂[n + 1]
thus (Partial_Sums (0c ExpSeq )) . (n + 1) = 1r + ((0c ExpSeq ) . (n + 1)) by A12, COMSEQ_3:def 7
.= 1r + ((((0c ExpSeq ) . n) * 0c ) / ((n + 1) + (0 * <i> ))) by Th4
.= 1 ; :: thesis: verum

end;

A13: for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A10, A11);
thus ( 0c ExpSeq is absolutely_summable & Sum (0c ExpSeq ) = 1r ) by A8, A13, COMSEQ_2:10, COMSEQ_3:def 11; :: thesis: verum