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