:: deftheorem Def3 defines multcpfunc LPSPACC1:def 3 :
for A being non empty set
for b₂ being BinOp of (PFuncs (A,COMPLEX)) holds
( b₂ = multcpfunc A iff for f, g being Element of PFuncs (A,COMPLEX) holds b₂ . (f,g) = f (#) g );