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)))
thus (RealFuncMult A) . (((RealFuncExtMult A) . (a,f)),g) = (RealFuncMult A) . ((multreal [;] (a,f)),g) by Def4
.= multreal .: ((multreal [;] (a,f)),g) by Def3
.= multreal [;] (a,(multreal .: (f,g))) by FUNCOP_1:100
.= (RealFuncExtMult A) . (a,(multreal .: (f,g))) by Def4
.= (RealFuncExtMult A) . (a,((RealFuncMult A) . (f,g))) by Def3 ; :: thesis: verum