theorem :: CLVECT_3:24

for X being ComplexHilbertSpace
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,m)).|| < r )