:: deftheorem PP defines Partial_Product RVSUM_4:def 2 :
for s, b₂ being Complex_Sequence holds
( b₂ = Partial_Product s iff ( b₂ . 0 = s . 0 & ( for n being Nat holds b₂ . (n + 1) = (b₂ . n) * (s . (n + 1)) ) ) );