theorem Th23: :: BHSP_4:23

for X being RealHilbertSpace
for seq being sequence of X holds
( seq is summable iff for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((Sum (seq,n)) - (Sum (seq,m))).|| < r )