let s be Real_Sequence; :: thesis: ( ( for n being Nat holds 0 <= s . n ) implies Partial_Sums s is non-decreasing )
assume A1: for n being Nat holds 0 <= s . n ; :: thesis: Partial_Sums s is non-decreasing

now :: thesis: for n being Nat holds (Partial_Sums s) . n <= (Partial_Sums s) . (n + 1)

let n be Nat; :: thesis: (Partial_Sums s) . n <= (Partial_Sums s) . (n + 1)
0 <= s . (n + 1) by A1;
then 0 + ((Partial_Sums s) . n) <= (s . (n + 1)) + ((Partial_Sums s) . n) by XREAL_1:6;
hence (Partial_Sums s) . n <= (Partial_Sums s) . (n + 1) by Def1; :: thesis: verum

end;

hence Partial_Sums s is non-decreasing ; :: thesis: verum