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