let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for n, m being Nat holds ||.(Sum (seq,m,n)).|| <= |.(Sum (||.seq.||,m,n)).|
let seq be sequence of X; :: thesis: for n, m being Nat holds ||.(Sum (seq,m,n)).|| <= |.(Sum (||.seq.||,m,n)).|
let n, m be Nat; :: thesis: ||.(Sum (seq,m,n)).|| <= |.(Sum (||.seq.||,m,n)).|
||.((Sum (seq,m)) - (Sum (seq,n))).|| <= |.((Sum (||.seq.||,m)) - (Sum (||.seq.||,n))).| by Th40;
hence ||.(Sum (seq,m,n)).|| <= |.(Sum (||.seq.||,m,n)).| by SERIES_1:def 6; :: thesis: verum