for s, s1 being Real_Sequence st ( for n being Nat holds
( s . n > 0 & s1 . n = (s . (n + 1)) / (s . n) ) ) & s1 is convergent & lim s1 < 1 holds
s is summable