theorem Th24: :: LOPBAN_3:24

for X being RealBanachSpace
for seq being sequence of X holds
( seq is summable iff for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p ) by Th5, LOPBAN_1:def 15, Th4;