:: deftheorem Def7 defines Sum RMOD_4:def 7 :
for R being Ring
for V being RightMod of R
for L being Linear_Combination of V
for b₄ being Vector of V holds
( b₄ = Sum L iff ex F being FinSequence of V st
( F is one-to-one & rng F = Carrier L & b₄ = Sum (L (#) F) ) );