:: deftheorem Def5 defines dom2tuple ACKERMAN:def 5 :
for D being set
for f being BinOp of D
for b₃ being Function holds
( ( not D is empty implies ( b₃ = dom2tuple f iff ( dom b₃ = 2 -tuples_on D & ( for x, y being object st [x,y] in dom f holds
b₃ . <*x,y*> = f . (x,y) ) ) ) ) & ( D is empty implies ( b₃ = dom2tuple f iff b₃ = {} ) ) );