theorem Th25: :: FUNCT_2:25

for X, Y being set
for f being Function of X,Y st f is one-to-one & rng f = Y holds
f " is Function of Y,X