:: deftheorem Def2 defines ComplexFuncMult CFUNCDOM:def 2 :
for A being set
for b₂ being BinOp of (Funcs (A,COMPLEX)) holds
( b₂ = ComplexFuncMult A iff for f, g being Element of Funcs (A,COMPLEX) holds b₂ . (f,g) = multcomplex .: (f,g) );