let A be set ; :: thesis: 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)))
let f, g, h be Element of Funcs (A,REAL); :: thesis: for a being Real holds (RealFuncMult A) . (((RealFuncExtMult A) . (a,f)),g) = (RealFuncExtMult A) . (a,((RealFuncMult A) . (f,g)))
let a be Real; :: thesis: (RealFuncMult A) . (((RealFuncExtMult A) . (a,f)),g) = (RealFuncExtMult A) . (a,((RealFuncMult A) . (f,g)))
reconsider aa = a as Element of REAL by XREAL_0:def 1;
thus (RealFuncMult A) . (((RealFuncExtMult A) . (a,f)),g) = (RealFuncMult A) . ((multreal [;] (a,f)),g) by Def3
.= multreal .: ((multreal [;] (aa,f)),g) by Def2
.= multreal [;] (aa,(multreal .: (f,g))) by FUNCOP_1:85
.= (RealFuncExtMult A) . (a,(multreal .: (f,g))) by Def3
.= (RealFuncExtMult A) . (a,((RealFuncMult A) . (f,g))) by Def2 ; :: thesis: verum