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