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:54, FUNCT_1:61; :: according to ALGSPEC1:def 2 :: thesis: verum