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