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 3;
then A6: g . (f . x) in dom f by Th25;
f . (g . (f . x)) = f . x by A5, Th25;
then x = g . (f . x) by A1, A4, A6, FUNCT_1:def 4;
hence x in rng g by A2, A5, FUNCT_1:def 3; :: 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 that
A7: x in dom f and
A8: y in dom g ; :: thesis: ( f . x = y iff g . y = x )
A9: g . y in rng g by A8, FUNCT_1:def 3;
f . (g . y) = y by A2, A8, Th25;
hence ( f . x = y iff g . y = x ) by A1, A3, A7, A9, FUNCT_1:def 4; :: thesis: verum

end;

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