:: deftheorem Def12 defines Sum RLVECT_1:def 12 :
for V being non empty addLoopStr
for F being the carrier of b₁ -valued FinSequence
for b₃ being Element of V holds
( b₃ = Sum F iff ex f being sequence of V st
( b₃ = f . (len F) & f . 0 = 0. V & ( for j being Nat
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) );