for n being Nat
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