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 13 :: 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