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