:: deftheorem Def6 defines multiplication NOMIN_5:def 6 :
for A being set st A is complex-containing holds
for b₂ being Function of [:A,A:],A holds
( b₂ = multiplication A iff for x, y being object st x in A & y in A holds
b₂ . (x,y) = multiplication (x,y) );