theorem Th42: :: FUNCT_4:42

for f being Function
for x, y being object holds
( [x,y] in dom f iff [y,x] in dom (~ f) )