:: deftheorem Def29 defines LinComb ZMODUL02:def 29 :
for R being Ring
for V being LeftMod of R
for b₃ being set holds
( b₃ = LinComb V iff for x being set holds
( x in b₃ iff x is Linear_Combination of V ) );