theorem :: FUNCSDOM:30

for A being non empty set
for f being Element of Funcs (A,REAL)
for a being Real holds (RealFuncExtMult A) . (a,f) = a (#) f