theorem Th9: :: FUNCSDOM:9

for A being set
for f being Element of Funcs (A,REAL) holds (RealFuncMult A) . ((RealFuncUnit A),f) = f