let X, Y be set ; :: thesis: for f being Function of X,Y st f is one-to-one & rng f = Y holds
f " is Function of Y,X
let f be Function of X,Y; :: thesis: ( f is one-to-one & rng f = Y implies f " is Function of Y,X )
assume that
A1: f is one-to-one and
A2: rng f = Y ; :: thesis: f " is Function of Y,X
A3: rng (f " ) c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (f " ) or x in X )
assume x in rng (f " ) ; :: thesis: x in X
then x in dom f by A1, FUNCT_1:55;
hence x in X ; :: thesis: verum

end;

dom (f " ) = Y by A1, A2, FUNCT_1:55;
then reconsider R = f " as Relation of Y,X by A3, RELSET_1:11;
R is quasi_total

proof

per cases not ( X = {} & not Y = {} & not ( X = {} & Y <> {} ) ) ;
:: according to FUNCT_2:def 1

case ( X = {} implies Y = {} ) ; :: thesis: Y = dom R

thus Y = dom R by A1, A2, FUNCT_1:55; :: thesis: verum

end;

case ( X = {} & Y <> {} ) ; :: thesis: R = {}

then rng f = {} ;
then dom (f " ) = {} by A1, FUNCT_1:54;
hence R = {} ; :: thesis: verum

end;

end;

end;

hence f " is Function of Y,X ; :: thesis: verum