:: deftheorem SUM defines Sum BAGORD_2:def 7 :
for I being set
for f being Bags b₁ -valued FinSequence
for b₃ being bag of I holds
( b₃ = Sum f iff ex F being Function of NAT,(Bags I) st
( b₃ = F . (len f) & F . 0 = EmptyBag I & ( for i being Nat
for b being bag of I st i < len f & b = f . (i + 1) holds
F . (i + 1) = (F . i) + b ) ) );