theorem :: CLVECT_3:38

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