for rseq being Real_Sequence st rseq is absolutely_summable & Sum (abs rseq) = 0 holds
for n being Nat holds rseq . n = 0