:: deftheorem Def1 defines Partial_Sums MESFUNC9:def 1 :
for s being ext-real-valued Function
for b₂ being ExtREAL_sequence holds
( b₂ = Partial_Sums s iff ( b₂ . 0 = s . 0 & ( for n being Nat holds b₂ . (n + 1) = (b₂ . n) + (s . (n + 1)) ) ) );