theorem Th14: :: FUNCSDOM:14

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