let f be Function; :: thesis:
thus ( ( for y being object st y in rng f holds
ex x being object st f " {y} = {x} ) implies f is one-to-one ) :: thesis:

assume A1: for y being object st y in rng f holds
ex x being object st f " {y} = {x} ; :: thesis:
let x1 be object ; :: according to FUNCT_1:def 4 :: thesis:
let x2 be object ; :: thesis:
assume that
A2: x1 in dom f and
A3: x2 in dom f ; :: thesis:
f . x1 in rng f by A2, Def3;
then consider y1 being object such that
A4: f " {(f . x1)} = {y1} by A1;
f . x2 in rng f by A3, Def3;
then consider y2 being object such that
A5: f " {(f . x2)} = {y2} by A1;
f . x1 in {(f . x1)} by TARSKI:def 1;
then x1 in {y1} by A2, A4, Def7;
then A6: y1 = x1 by TARSKI:def 1;
f . x2 in {(f . x2)} by TARSKI:def 1;
then x2 in {y2} by A3, A5, Def7;
hence ( not f . x1 = f . x2 or x1 = x2 ) by A4, A5, A6, TARSKI:def 1; :: thesis:

end;

assume A7: f is one-to-one ; :: thesis:
let y be object ; :: thesis:
assume y in rng f ; :: thesis:
then consider x being object such that
A8: ( x in dom f & y = f . x ) by Def3;
take x ; :: thesis:
for z being object holds
( z in f " {y} iff z = x )

let z be object ; :: thesis:
thus ( z in f " {y} implies z = x ) :: thesis:

end;

y in {y} by TARSKI:def 1;
hence ( z = x implies z in f " {y} ) by A8, Def7; :: thesis:

end;