:: deftheorem Def4 defines FuncMult CLOPBAN2:def 4 :
for X being ComplexNormSpace
for b₂ being BinOp of (BoundedLinearOperators (X,X)) holds
( b₂ = FuncMult X iff for f, g being Element of BoundedLinearOperators (X,X) holds b₂ . (f,g) = f * g );