:: deftheorem Def1 defines Partial_Sums SERIES_1:def 1 :
for s, b₂ being complex-valued ManySortedSet of NAT holds
( b₂ = Partial_Sums s iff ( b₂ . 0 = s . 0 & ( for n being Nat holds b₂ . (n + 1) = (b₂ . n) + (s . (n + 1)) ) ) );