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