theorem :: SERIES_3:45

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 > 0 & (Partial_Product s) . n < 1 )