:: deftheorem Def1 defines FuncExtMult CLOPBAN1:def 1 :
for X being non empty set
for Y being ComplexLinearSpace
for b₃ being Function of [:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) holds
( b₃ = FuncExtMult (X,Y) iff for c being Complex
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (b₃ . [c,f]) . x = c * (f . x) );