let A be set ; :: thesis: for f, g, h being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (f,((RealFuncAdd A) . (g,h))) = (RealFuncAdd A) . (((RealFuncAdd A) . (f,g)),h)
let f, g, h be Element of Funcs (A,REAL); :: thesis: (RealFuncAdd A) . (f,((RealFuncAdd A) . (g,h))) = (RealFuncAdd A) . (((RealFuncAdd A) . (f,g)),h)
thus (RealFuncAdd A) . (f,((RealFuncAdd A) . (g,h))) = (RealFuncAdd A) . (f,(addreal .: (g,h))) by Def1
.= addreal .: (f,(addreal .: (g,h))) by Def1
.= addreal .: ((addreal .: (f,g)),h) by FUNCOP_1:61
.= (RealFuncAdd A) . ((addreal .: (f,g)),h) by Def1
.= (RealFuncAdd A) . (((RealFuncAdd A) . (f,g)),h) by Def1 ; :: thesis: verum