:: deftheorem Def16 defines C_LCMult CONVEX4:def 16 :
for V being non empty CLSStruct
for b₂ being Function of [:COMPLEX,(C_LinComb V):],(C_LinComb V) holds
( b₂ = C_LCMult V iff for a being Complex
for e being Element of C_LinComb V holds b₂ . [a,e] = a * (@ e) );