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