theorem :: BHSP_4:40

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