:: deftheorem EXNDef defines ex1234/\ LATWAL_2:def 15 :
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 );