for n being Nat
for s being Real_Sequence st ( for n being Nat holds s . n > 0 ) holds
(Partial_Product s) . n > 0