for s being Real_Sequence st s is summable holds
( s is convergent & lim s = 0 )