theorem Th10: :: CLVECT_3:10

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
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).|| < r ) by CLVECT_2:65, CLVECT_2:58, CLVECT_2:def 11;