:: deftheorem Def13 defines Partial_Sums TOPALG_6:def 13 :
for T being TopStruct
for f, b₃ being FinSequence of Curves T holds
( b₃ = Partial_Sums f iff ( len f = len b₃ & f . 1 = b₃ . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₃ . (i + 1) = (b₃ /. i) + (f /. (i + 1)) ) ) );