:: deftheorem Def1 defines Sum CARDFIL3:def 4 :
for I being non empty set
for L being AbGroup
for x being the carrier of b₂ -valued ManySortedSet of I
for J being Element of Fin I
for b₅ being Element of L holds
( b₅ = Sum (x,J) iff ex p being one-to-one FinSequence of I st
( rng p = J & b₅ = the addF of L "**" (# (p,x)) ) );