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

now

let n be Element of 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:8;
hence (Partial_Sums s) . n <= (Partial_Sums s) . (n + 1) by Def1; :: thesis: verum

end;

hence Partial_Sums s is non-decreasing by SEQM_3:def 13; :: thesis: verum