let D be non empty set ; :: thesis: addpfunc D is associative
let F1, F2, F3 be Element of PFuncs D,REAL ; :: according to BINOP_1:def 14 :: thesis: (addpfunc D) . F1,((addpfunc D) . F2,F3) = (addpfunc D) . ((addpfunc D) . F1,F2),F3
set o = addpfunc D;
thus (addpfunc D) . F1,((addpfunc D) . F2,F3) = (addpfunc D) . F1,(F2 + F3) by Def4
.= F1 + (F2 + F3) by Def4
.= (F1 + F2) + F3 by RFUNCT_1:19
.= ((addpfunc D) . F1,F2) + F3 by Def4
.= (addpfunc D) . ((addpfunc D) . F1,F2),F3 by Def4 ; :: thesis: verum