:: deftheorem Def3 defines addition NOMIN_5:def 3 :
for x, y being object st x is Complex & y is Complex holds
for b₃ being Complex holds
( b₃ = addition (x,y) iff ex x1, y1 being Complex st
( x1 = x & y1 = y & b₃ = x1 + y1 ) );