:: deftheorem Def18 defines LCMult RLVECT_2:def 18 :
for V being RealLinearSpace
for b₂ being Function of [:REAL,(LinComb V):],(LinComb V) holds
( b₂ = LCMult V iff for a being Real
for e being Element of LinComb V holds b₂ . [a,e] = a * (@ e) );