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