for X, Y being non empty set
for f being Function of X,Y
for g being Function of Y,X st ( for x being Element of X holds g . (f . x) = x ) & ( for y being Element of Y holds f . (g . y) = y ) holds
( f is one-to-one & f is onto & g is one-to-one & g is onto & g = f " & f = g " )