let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for n being Element of NAT holds (Partial_Sums ||.seq.||) . n >= 0
let seq be sequence of X; :: thesis: for n being Element of NAT holds (Partial_Sums ||.seq.||) . n >= 0
let n be Element of NAT ; :: thesis: (Partial_Sums ||.seq.||) . n >= 0
||.(seq . 0 ).|| >= 0 by CSSPACE:46;
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:21; :: thesis: verum