let rseq be Real_Sequence; :: thesis: ( rseq is absolutely_summable & Sum (abs rseq) = 0 implies for n being Element of NAT holds rseq . n = 0 )
assume that
A1: rseq is absolutely_summable and
A2: Sum (abs rseq) = 0 ; :: thesis: for n being Element of NAT holds rseq . n = 0
reconsider arseq = abs rseq as Real_Sequence ;
A3: arseq is summable by A1, SERIES_1:def 5;
A4: for n being Element of NAT holds 0 <= (abs rseq) . n

proof

let n be Element of NAT ; :: thesis: 0 <= (abs rseq) . n
0 <= abs (rseq . n) by COMPLEX1:132;
hence 0 <= (abs rseq) . n by SEQ_1:16; :: thesis: verum

end;

for n being Element of NAT holds rseq . n = 0

proof

let n be Element of NAT ; :: thesis: rseq . n = 0
(abs rseq) . n = 0 by A2, A3, A4, RSSPACE:21;
then abs (rseq . n) = 0 by SEQ_1:16;
hence rseq . n = 0 by ABSVALUE:7; :: thesis: verum

end;

hence for n being Element of NAT holds rseq . n = 0 ; :: thesis: verum