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))).|