let X be RealUnitarySpace; :: 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 BHSP_1:28;
then A1: ||.seq.|| . 0 >= 0 by BHSP_2:def 3;
(Partial_Sums ||.seq.||) . 0 <= (Partial_Sums ||.seq.||) . n by Th37, SEQM_3:11;
hence (Partial_Sums ||.seq.||) . n >= 0 by A1, SERIES_1:def 1; :: thesis: verum