for X, Y being set
for f being PartFunc of X,Y st f is one-to-one holds
f " is PartFunc of Y,X