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
((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2) >= 0
let s be Real_Sequence; :: thesis: ( ( for n being Nat holds
( s . n > 0 & s . n >= s . (n - 1) ) ) implies ((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2) >= 0 )
assume for n being Nat holds
( s . n > 0 & s . n >= s . (n - 1) ) ; :: thesis: ((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2) >= 0
then ((n + 1) * (s . (n + 1))) / (n + 1) >= ((Partial_Sums s) . n) / (n + 1) by Th38, XREAL_1:72;
then s . (n + 1) >= ((Partial_Sums s) . n) / (n + 1) by XCMPLX_1:89;
then (s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1)) >= 0 by XREAL_1:48;
hence ((s . (n + 1)) - (((Partial_Sums s) . n) / (n + 1))) / (n + 2) >= 0 ; :: thesis: verum