:: deftheorem Def1 defines Sum RMOD_4:def 1 :
for R being Ring
for V being RightMod of R
for T being finite Subset of V
for b₄ being Vector of V holds
( b₄ = Sum T iff ex F being FinSequence of V st
( rng F = T & F is one-to-one & b₄ = Sum F ) );