let X be RealUnitarySpace; :: thesis: for seq being sequence of X holds Partial_Sums ||.seq.|| is non-decreasing
let seq be sequence of X; :: thesis: Partial_Sums ||.seq.|| is non-decreasing
now :: thesis: for n being Nat holds (Partial_Sums ||.seq.||) . n <= (Partial_Sums ||.seq.||) . (n + 1)
let n be Nat; :: thesis: (Partial_Sums ||.seq.||) . n <= (Partial_Sums ||.seq.||) . (n + 1)
||.(seq . (n + 1)).|| >= 0 by BHSP_1:28;
then ||.seq.|| . (n + 1) >= 0 by BHSP_2:def 3;
then 0 + ((Partial_Sums ||.seq.||) . n) <= (||.seq.|| . (n + 1)) + ((Partial_Sums ||.seq.||) . n) by XREAL_1:6;
hence (Partial_Sums ||.seq.||) . n <= (Partial_Sums ||.seq.||) . (n + 1) by SERIES_1:def 1; :: thesis: verum
end;
hence Partial_Sums ||.seq.|| is non-decreasing ; :: thesis: verum