theorem Th16: :: FUNCSDOM:16

for A being set
for f, g, h being Element of Funcs (A,REAL)
for a being Real holds (RealFuncMult A) . (((RealFuncExtMult A) . (a,f)),g) = (RealFuncExtMult A) . (a,((RealFuncMult A) . (f,g)))