:: deftheorem Def1 defines Partial_Product SERIES_3:def 1 :
for s, b₂ being Real_Sequence holds
( b₂ = Partial_Product s iff ( b₂ . 0 = s . 0 & ( for n being Nat holds b₂ . (n + 1) = (b₂ . n) * (s . (n + 1)) ) ) );