let rseq be Real_Sequence; :: thesis: ( rseq is absolutely_summable & Sum (abs rseq) = 0 implies for n being Nat holds rseq . n = 0 )
assume that
A1: rseq is absolutely_summable and
A2: Sum (abs rseq) = 0 ; :: thesis: for n being Nat holds rseq . n = 0
reconsider arseq = abs rseq as Real_Sequence ;
A3: for n being Nat holds 0 <= (abs rseq) . n

proof

let n be Nat; :: thesis: 0 <= (abs rseq) . n
0 <= |.(rseq . n).| by COMPLEX1:46;
hence 0 <= (abs rseq) . n by SEQ_1:12; :: thesis: verum

end;

A4: arseq is summable by A1, SERIES_1:def 4;
let n be Nat; :: thesis: rseq . n = 0
(abs rseq) . n = 0 by A2, A4, A3, RSSPACE:17;
then |.(rseq . n).| = 0 by SEQ_1:12;
hence rseq . n = 0 by ABSVALUE:2; :: thesis: verum