theorem :: FUNCT_2:31

for X, Y being set
for f being Function of X,Y st Y <> {} & ex g being Function of Y,X st g * f = id X holds
f is one-to-one