let X, Y be set ; :: thesis: for f being PartFunc of X,Y st f is one-to-one holds
f " is PartFunc of Y,X
let f be PartFunc of X,Y; :: thesis: ( f is one-to-one implies f " is PartFunc of Y,X )
assume A1: f is one-to-one ; :: thesis: f " is PartFunc of Y,X
rng f c= Y by RELAT_1:def 19;
then A2: dom (f ") c= Y by A1, FUNCT_1:33;
dom f c= X ;
then rng (f ") c= X by A1, FUNCT_1:33;
hence f " is PartFunc of Y,X by A2, RELSET_1:4; :: thesis: verum