theorem :: SERIES_3:49

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