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
( dom f c= X & rng f c= Y ) by RELAT_1:def 19;
then ( dom (f " ) c= Y & rng (f " ) c= X ) by A1, FUNCT_1:55;
hence f " is PartFunc of Y,X by RELSET_1:11; :: thesis: verum