:: deftheorem Def3 defines Partial_Sums MESFUN9C:def 3 :
for X being non empty set
for F, b₃ being Functional_Sequence of X,COMPLEX holds
( b₃ = Partial_Sums F iff ( b₃ . 0 = F . 0 & ( for n being Nat holds b₃ . (n + 1) = (b₃ . n) + (F . (n + 1)) ) ) );