:: deftheorem Def4 defines multcomplexcpfunc LPSPACC1:def 4 :
for A being non empty set
for b₂ being Function of [:COMPLEX,(PFuncs (A,COMPLEX)):],(PFuncs (A,COMPLEX)) holds
( b₂ = multcomplexcpfunc A iff for a being Complex
for f being Element of PFuncs (A,COMPLEX) holds b₂ . (a,f) = a (#) f );