for X, Y being set
for f being Function of X,Y st f is bijective holds
f " is Function of Y,X