let X, Y be set ; :: thesis: ( ex f being Function st
( f is one-to-one & dom f = X & rng f = Y ) implies ex f being Function st
( f is one-to-one & dom f = Y & rng f = X ) )
given f being Function such that A25: ( f is one-to-one & dom f = X & rng f = Y ) ; :: thesis: ex f being Function st
( f is one-to-one & dom f = Y & rng f = X )
take f " ; :: thesis: ( f " is one-to-one & dom (f ") = Y & rng (f ") = X )
thus ( f " is one-to-one & dom (f ") = Y & rng (f ") = X ) by A25, FUNCT_1:33; :: thesis: verum