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 object ; :: 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:33;
hence x in X ; :: thesis: verum

end;

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

proof

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

case X <> {} ; :: thesis: Y = dom R

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

end;

case X = {} ; :: thesis: R = {}

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

end;

end;

end;

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