theorem :: ALGSPEC1:26

for f being Function st f is one-to-one holds
for g being rng-retract of f holds g = f "