theorem :: BHSP_4:41

for X being RealUnitarySpace
for seq being sequence of X
for n, m being Nat holds ||.(Sum (seq,m,n)).|| <= |.(Sum (||.seq.||,m,n)).| by Th39;