:: deftheorem Def4 defines addpfunc RFUNCT_3:def 4 :
for D being non empty set
for b₂ being BinOp of (PFuncs (D,REAL)) holds
( b₂ = addpfunc D iff for F1, F2 being Element of PFuncs (D,REAL) holds b₂ . (F1,F2) = F1 + F2 );