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