:: deftheorem Def33 defines LCMult ZMODUL02:def 33 :
for R being Ring
for V being LeftMod of R
for b₃ being Function of [: the carrier of R,(LinComb V):],(LinComb V) holds
( b₃ = LCMult V iff for a being Element of R
for e being Element of LinComb V holds b₃ . [a,e] = a * (@ e) );