let a be Real_Sequence; :: thesis: ( ( for n being Nat holds 0 <= a . n ) implies for n being Nat holds a . n <= (Partial_Sums a) . n )

assume A1: for n being Nat holds 0 <= a . n ; :: thesis: for n being Nat holds a . n <= (Partial_Sums a) . n

defpred S_{1}[ Nat] means a . $1 <= (Partial_Sums a) . $1;

A2: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
by SERIES_1:def 1;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A4, A2);

hence for n being Nat holds a . n <= (Partial_Sums a) . n ; :: thesis: verum

assume A1: for n being Nat holds 0 <= a . n ; :: thesis: for n being Nat holds a . n <= (Partial_Sums a) . n

defpred S

A2: for n being Nat st S

S

proof

A4:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume S_{1}[n]
; :: thesis: S_{1}[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:6;

0 <= a . n by A1;

then 0 + (a . (n + 1)) <= (a . n) + (a . (n + 1)) by XREAL_1:6;

hence S_{1}[n + 1]
by A3, XXREAL_0:2; :: thesis: verum

end;assume S

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:6;

0 <= a . n by A1;

then 0 + (a . (n + 1)) <= (a . n) + (a . (n + 1)) by XREAL_1:6;

hence S

for n being Nat holds S

hence for n being Nat holds a . n <= (Partial_Sums a) . n ; :: thesis: verum