theorem Th39: :: BHSP_4:39

for X being RealUnitarySpace
for seq being sequence of X
for n, m being Nat holds ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= |.(((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)).|