let X, Y be set ; 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; ( 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
; f " is Function of Y,X
A3:
rng (f ") c= X
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
hence
f " is Function of Y,X
; verum