:: deftheorem Def5 defines addcpfunc LPSPACC1:def 5 :
for D being non empty set
for b₂ being BinOp of (PFuncs (D,COMPLEX)) holds
( b₂ = addcpfunc D iff for F1, F2 being Element of PFuncs (D,COMPLEX) holds b₂ . (F1,F2) = F1 + F2 );