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