theorem :: FUNCT_2:55

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