let seq be Complex_Sequence; :: thesis:
assume that
A1: seq is absolutely_summable and
A2: Sum |.seq.| = 0 ; :: thesis:
A3: for n being Nat holds (Partial_Sums |.seq.|) . n <= Sum |.seq.|

proof

let n be Nat; :: thesis:
(Partial_Sums |.seq.|) . n <= lim (Partial_Sums |.seq.|) by A1, SEQ_4:37;
hence (Partial_Sums |.seq.|) . n <= Sum |.seq.| by SERIES_1:def 3; :: thesis:

end;

A4: now :: thesis:

assume ex n being Nat st |.seq.| . n <> 0 ; :: thesis:
then consider n1 being Nat such that
A5: |.seq.| . n1 <> 0 ;
A6: for n being Nat holds 0 <= (Partial_Sums |.seq.|) . n

proof

let n be Nat; :: thesis:
|.seq.| . 0 = |.(seq . 0).| by VALUED_1:18;
then A7: 0 <= |.seq.| . 0 by COMPLEX1:46;
( n = n + 0 & (Partial_Sums |.seq.|) . 0 = |.seq.| . 0 ) by SERIES_1:def 1;
hence 0 <= (Partial_Sums |.seq.|) . n by A7, SEQM_3:5; :: thesis:

end;

(Partial_Sums |.seq.|) . n1 > 0

proof

now :: thesis:

per cases ;

case n1 = 0 ; :: thesis:

then (Partial_Sums |.seq.|) . n1 <> 0 by A5, SERIES_1:def 1;
hence (Partial_Sums |.seq.|) . n1 > 0 by A6; :: thesis:

end;

case A8: n1 <> 0 ; :: thesis:

set nn = n1 - 1;
|.seq.| . n1 = |.(seq . n1).| by VALUED_1:18;
then A9: ( (n1 - 1) + 1 = n1 & 0 <= |.seq.| . n1 ) by COMPLEX1:46;
0 + 1 <= n1 by A8, INT_1:7;
then A10: n1 - 1 in NAT by INT_1:5;
then 0 <= (Partial_Sums |.seq.|) . (n1 - 1) by A6;
then (|.seq.| . n1) + 0 <= (|.seq.| . n1) + ((Partial_Sums |.seq.|) . (n1 - 1)) by XREAL_1:7;
hence (Partial_Sums |.seq.|) . n1 > 0 by A5, A10, A9, SERIES_1:def 1; :: thesis:

end;

end;

end;

hence (Partial_Sums |.seq.|) . n1 > 0 ; :: thesis:

end;

hence contradiction by A2, A3; :: thesis:

end;

for n being Nat holds seq . n = 0c

proof

let n be Nat; :: thesis:
0 = |.seq.| . n by A4
.= |.(seq . n).| by VALUED_1:18 ;
hence seq . n = 0c by COMPLEX1:45; :: thesis:

end;

hence for n being Nat holds seq . n = 0c ; :: thesis: