theorem :: SERIES_5:51

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