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