for s being Real_Sequence st s is absolutely_summable holds
s is summable ;