let a be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds 0 <= a . n ) implies for n being Element of NAT holds a . n <= (Partial_Sums a) . n )
assume A1: for n being Element of NAT holds 0 <= a . n ; :: thesis: for n being Element of NAT holds a . n <= (Partial_Sums a) . n
defpred S₁[ Element of NAT ] means a . $1 <= (Partial_Sums a) . $1;
A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then A3: ( (Partial_Sums a) . (n + 1) = ((Partial_Sums a) . n) + (a . (n + 1)) & (a . n) + (a . (n + 1)) <= ((Partial_Sums a) . n) + (a . (n + 1)) ) by SERIES_1:def 1, XREAL_1:8;
0 <= a . n by A1;
then 0 + (a . (n + 1)) <= (a . n) + (a . (n + 1)) by XREAL_1:8;
hence S₁[n + 1] by A3, XXREAL_0:2; :: thesis: verum

end;

A4: S₁[ 0 ] by SERIES_1:def 1;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A2);
hence for n being Element of NAT holds a . n <= (Partial_Sums a) . n ; :: thesis: verum