theorem Th10: :: BHSP_4:10

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
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ) by BHSP_3:2, BHSP_3:def 4;