let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for n being Nat holds ||.(Sum (seq,n)).|| <= Sum (||.seq.||,n)
let seq be sequence of X; :: thesis: for n being Nat holds ||.(Sum (seq,n)).|| <= Sum (||.seq.||,n)
let n be 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 5; :: thesis: verum