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