:: deftheorem Def4 defines Partial_Sums MESFUNC9:def 4 :
for X being non empty set
for F, b₃ being Functional_Sequence of X,ExtREAL holds
( b₃ = Partial_Sums F iff ( b₃ . 0 = F . 0 & ( for n being Nat holds b₃ . (n + 1) = (b₃ . n) + (F . (n + 1)) ) ) );