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 7; :: thesis: verum