:: deftheorem Def2 defines FuncExtMult LOPBAN_1:def 2 :
for X being non empty set
for Y being RealLinearSpace
for b₃ being Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) holds
( b₃ = FuncExtMult (X,Y) iff for a being Real
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (b₃ . [a,f]) . x = a * (f . x) );