let D be non empty set ; addpfunc D is associative
let F1, F2, F3 be Element of PFuncs (D,REAL); BINOP_1:def 3 (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
; verum