let f be Function; :: thesis: ( ( for y being object st y in rng f holds
ex x being object st f " {y} = {x} ) iff f is one-to-one )
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: ( f is one-to-one implies for y being object st y in rng f holds
ex x being object st f " {y} = {x} )

proof

assume A1: for y being object st y in rng f holds
ex x being object st f " {y} = {x} ; :: thesis: f is one-to-one
let x1 be object ; :: according to FUNCT_1:def 4 :: thesis: for x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
let x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A2: x1 in dom f and
A3: x2 in dom f ; :: thesis: ( not f . x1 = f . x2 or x1 = x2 )
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: verum

end;

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

proof

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

proof

assume A9: z in f " {y} ; :: thesis: z = x
then f . z in {y} by Def7;
then A10: f . z = y by TARSKI:def 1;
z in dom f by A9, Def7;
hence z = x by A7, A8, A10; :: thesis: verum

end;

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

end;

hence f " {y} = {x} by TARSKI:def 1; :: thesis: verum