:: deftheorem Def4 defines dom2tuple ACKERMAN:def 4 :
for f, b₂ being Function holds
( ( not f is empty implies ( b₂ = dom2tuple f iff ( dom b₂ = 1 -tuples_on (dom f) & ( for x being object st x in dom f holds
b₂ . <*x*> = f . x ) ) ) ) & ( f is empty implies ( b₂ = dom2tuple f iff b₂ = {} ) ) );