for s being Real_Sequence holds
( s is summable iff for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r ) by SEQ_4:41;