theorem Th40: :: CLVECT_3:40

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