theorem Th45: :: FUNCT_4:45

for X, Y being set
for f being Function st dom f c= [:X,Y:] holds
dom (~ f) c= [:Y,X:]