:: deftheorem Def5 defines Linear_Combination RMOD_4:def 5 :
for R being Ring
for V being RightMod of R
for A being Subset of V
for b₄ being Linear_Combination of V holds
( b₄ is Linear_Combination of A iff Carrier b₄ c= A );