for f being Function holds
( proj1 (dom f) = proj2 (dom (~ f)) & proj2 (dom f) = proj1 (dom (~ f)) )