let f be Function; :: thesis: ( f is one-to-one implies f " is rng-retract of f )
assume f is one-to-one ; :: thesis: f " is rng-retract of f
hence ( dom (f ") = rng f & f * (f ") = id (rng f) ) by FUNCT_1:32, FUNCT_1:39; :: according to ALGSPEC1:def 2 :: thesis: verum