for S being 1-sorted
for T being non empty 1-sorted
for f being Function of S,T st f is bijective holds
f " is bijective