:: deftheorem Def2 defines Sum RLVECT_2:def 2 :
for V being non empty addLoopStr
for T being finite Subset of V st V is Abelian & V is add-associative & V is right_zeroed holds
for b₃ being Element of V holds
( b₃ = Sum T iff ex F being FinSequence of the carrier of V st
( rng F = T & F is one-to-one & b₃ = Sum F ) );