theorem :: SERIES_1:35

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