theorem Th25: :: LOPBAN_3:25

for X being RealNormSpace
for s being sequence of X
for n, m being Nat st n <= m holds
||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= |.(((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n)).|