:: deftheorem Def1 defines Partial_Sums BHSP_4:def 1 :
for X being non empty addLoopStr
for seq, b₃ being sequence of X holds
( b₃ = Partial_Sums seq iff ( b₃ . 0 = seq . 0 & ( for n being Nat holds b₃ . (n + 1) = (b₃ . n) + (seq . (n + 1)) ) ) );