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