theorem Th13: :: FUNCSDOM:13

for a, b being Real
for A being set
for f being Element of Funcs (A,REAL) holds (RealFuncExtMult A) . (a,((RealFuncExtMult A) . (b,f))) = (RealFuncExtMult A) . ((a * b),f)