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