theorem :: SERIES_3:53

for n being Nat
for s being Real_Sequence st ( for n being Nat holds
( s . n > 0 & s . n >= s . (n - 1) ) ) holds
(Partial_Sums s) . n >= (n + 1) * ((n + 1) -root ((Partial_Product s) . n))