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 3 :: 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:8
.= ((addpfunc D) . (F1,F2)) + F3 by Def4
.= (addpfunc D) . (((addpfunc D) . (F1,F2)),F3) by Def4 ; :: thesis: verum