theorem :: ALGSPEC1:25

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