:: deftheorem Def1 defines ~ FUNCOP_1:def 1 :
for f, b₂ being Function holds
( b₂ = f ~ iff ( dom b₂ = dom f & ( for x being object st x in dom f holds
( ( for y, z being object st f . x = [y,z] holds
b₂ . x = [z,y] ) & ( f . x = b₂ . x or ex y, z being object st f . x = [y,z] ) ) ) ) );