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

( 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