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