:: deftheorem DEF13 defines Partial_Sums MEASUR11:def 11 :
for X being non empty set
for F being summable FinSequence of Funcs (X,ExtREAL)
for b₃ being FinSequence of Funcs (X,ExtREAL) holds
( b₃ = Partial_Sums F iff ( len F = len b₃ & F . 1 = b₃ . 1 & ( for n being Nat st 1 <= n & n < len F holds
b₃ . (n + 1) = (b₃ /. n) + (F /. (n + 1)) ) ) );