theorem Th39: :: CLVECT_3:39

for X being ComplexUnitarySpace
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)).|