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 Def2
.= addreal .: f,(addreal .: g,h) by Def2
.= addreal .: (addreal .: f,g),h by FUNCOP_1:76
.= (RealFuncAdd A) . (addreal .: f,g),h by Def2
.= (RealFuncAdd A) . ((RealFuncAdd A) . f,g),h by Def2 ; :: thesis: verum