let A be set ; :: thesis: for f, g, h being Element of Funcs A,REAL holds (RealFuncMult A) . f,((RealFuncMult A) . g,h) = (RealFuncMult A) . ((RealFuncMult A) . f,g),h
let f, g, h be Element of Funcs A,REAL ; :: thesis: (RealFuncMult A) . f,((RealFuncMult A) . g,h) = (RealFuncMult A) . ((RealFuncMult A) . f,g),h
thus (RealFuncMult A) . f,((RealFuncMult A) . g,h) = (RealFuncMult A) . f,(multreal .: g,h) by Def3
.= multreal .: f,(multreal .: g,h) by Def3
.= multreal .: (multreal .: f,g),h by FUNCOP_1:76
.= (RealFuncMult A) . (multreal .: f,g),h by Def3
.= (RealFuncMult A) . ((RealFuncMult A) . f,g),h by Def3 ; :: thesis: verum