for S, T being non empty 1-sorted
for f being Function of S,T st f is one-to-one & f is onto holds
( f * (f ") = id T & (f ") * f = id S & f " is one-to-one & f " is onto )