:: deftheorem defines Carrier RMOD_4:def 3 :
for R being Ring
for V being RightMod of R
for L being Linear_Combination of V holds Carrier L = { v where v is Vector of V : L . v <> 0. R } ;