let A be non empty set ; :: thesis: for f, g, h being Element of PFuncs A,REAL holds (addpfunc A) . f,((addpfunc A) . g,h) = (addpfunc A) . ((addpfunc A) . f,g),h
let f, g, h be Element of PFuncs A,REAL ; :: thesis: (addpfunc A) . f,((addpfunc A) . g,h) = (addpfunc A) . ((addpfunc A) . f,g),h
addpfunc A is associative by RFUNCT_3:17;
hence (addpfunc A) . f,((addpfunc A) . g,h) = (addpfunc A) . ((addpfunc A) . f,g),h by BINOP_1:def 3; :: thesis: verum