:: deftheorem Def4 defines multiplication NOMIN_5:def 4 :
for x, y being object st x is Complex & y is Complex holds
for b₃ being Complex holds
( b₃ = multiplication (x,y) iff ex x1, y1 being Complex st
( x1 = x & y1 = y & b₃ = x1 * y1 ) );