let n be Nat; :: thesis: for s being Real_Sequence st ( for n being Nat holds
( s . n > 0 & s . n >= s . (n - 1) ) ) holds
(n + 1) * (s . (n + 1)) >= (Partial_Sums s) . n
let s be Real_Sequence; :: thesis: ( ( for n being Nat holds
( s . n > 0 & s . n >= s . (n - 1) ) ) implies (n + 1) * (s . (n + 1)) >= (Partial_Sums s) . n )
defpred S₁[ Nat] means ($1 + 1) * (s . ($1 + 1)) >= (Partial_Sums s) . $1;
assume A1: for n being Nat holds
( s . n > 0 & s . n >= s . (n - 1) ) ; :: thesis: (n + 1) * (s . (n + 1)) >= (Partial_Sums s) . n
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume (n + 1) * (s . (n + 1)) >= (Partial_Sums s) . n ; :: thesis: S₁[n + 1]
then A3: ((Partial_Sums s) . n) + (s . (n + 1)) <= ((n + 1) * (s . (n + 1))) + (s . (n + 1)) by XREAL_1:6;
s . (n + 2) >= s . ((n + 2) - 1) by A1;
then (n + 2) * (s . (n + 2)) >= (n + 2) * (s . (n + 1)) by XREAL_1:64;
then ((Partial_Sums s) . n) + (s . (n + 1)) <= (n + 2) * (s . (n + 2)) by A3, XXREAL_0:2;
hence S₁[n + 1] by SERIES_1:def 1; :: thesis: verum

end;

s . 1 >= s . (1 - 1) by A1;
then A4: S₁[ 0 ] by SERIES_1:def 1;
for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A2);
hence (n + 1) * (s . (n + 1)) >= (Partial_Sums s) . n ; :: thesis: verum