let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for n being Nat holds (Partial_Sums ||.seq.||) . n >= 0
let seq be sequence of X; :: thesis: for n being Nat holds (Partial_Sums ||.seq.||) . n >= 0
let n be Nat; :: thesis: (Partial_Sums ||.seq.||) . n >= 0
||.(seq . 0).|| >= 0 by CSSPACE:44;
then ||.seq.|| . 0 >= 0 by CLVECT_2:def 3;
then (Partial_Sums ||.seq.||) . 0 >= 0 by SERIES_1:def 1;
hence (Partial_Sums ||.seq.||) . n >= 0 by Th35, SEQM_3:11; :: thesis: verum