let f be Function; :: thesis: ( f is one-to-one implies for g being rng-retract of f holds g = f " )
assume A1: f is one-to-one ; :: thesis: for g being rng-retract of f holds g = f "
let g be rng-retract of f; :: thesis: g = f "
A2: rng f = dom g by Def2;
A3: rng g = dom f

proof

thus rng g c= dom f by Th24; :: according to XBOOLE_0:def 10 :: thesis: dom f c= rng g
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in rng g )
assume A4: x in dom f ; :: thesis: x in rng g
then A5: f . x in rng f by FUNCT_1:def 5;
then ( f . (g . (f . x)) = f . x & g . (f . x) in dom f ) by Th25;
then x = g . (f . x) by A1, A4, FUNCT_1:def 8;
hence x in rng g by A2, A5, FUNCT_1:def 5; :: thesis: verum

end;

now

let x, y be set ; :: thesis: ( x in dom f & y in dom g implies ( f . x = y iff g . y = x ) )
assume A6: ( x in dom f & y in dom g ) ; :: thesis: ( f . x = y iff g . y = x )
then ( f . (g . y) = y & g . y in rng g ) by A2, Th25, FUNCT_1:def 5;
hence ( f . x = y iff g . y = x ) by A1, A3, A6, FUNCT_1:def 8; :: thesis: verum

end;

hence g = f " by A1, A2, A3, FUNCT_1:60; :: thesis: verum