for X, Y being set
for f being Function of X,Y
for g being Function of Y,X st g * f = id X holds
( f is one-to-one & g is onto )