:: deftheorem EXUDef defines ex1234\/ LATWAL_2:def 14 :
for b₁ being BinOp of {0,1,2,3,4} holds
( b₁ = ex1234\/ iff for x, y being Element of {0,1,2,3,4} holds b₁ . (x,y) = x ex1234"\/" y );