:: deftheorem Def3 defines RealFuncExtMult FUNCSDOM:def 3 :
for A being set
for b₂ being Function of [:REAL,(Funcs (A,REAL)):],(Funcs (A,REAL)) holds
( b₂ = RealFuncExtMult A iff for a being Real
for f being Element of Funcs (A,REAL) holds b₂ . (a,f) = multreal [;] (a,f) );