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

proof

thus ( ( for y being set ex x being set st f " {y} c= {x} ) implies for y being set st y in rng f holds
ex x being set st f " {y} = {x} ) :: thesis: ( ( for y being set st y in rng f holds
ex x being set st f " {y} = {x} ) implies for y being set ex x being set st f " {y} c= {x} )

proof

assume A1: for y being set ex x being set st f " {y} c= {x} ; :: thesis: for y being set st y in rng f holds
ex x being set st f " {y} = {x}
let y be set ; :: thesis: ( y in rng f implies ex x being set st f " {y} = {x} )
consider x being set such that
A2: f " {y} c= {x} by A1;
assume y in rng f ; :: thesis: ex x being set st f " {y} = {x}
then consider x1 being set such that
A3: x1 in dom f and
A4: y = f . x1 by Def5;
take x ; :: thesis: f " {y} = {x}
f . x1 in {y} by A4, TARSKI:def 1;
then f " {y} <> {} by A3, Def13;
hence f " {y} = {x} by A2, ZFMISC_1:39; :: thesis: verum

end;

assume A5: for y being set st y in rng f holds
ex x being set st f " {y} = {x} ; :: thesis: for y being set ex x being set st f " {y} c= {x}
let y be set ; :: thesis: ex x being set st f " {y} c= {x}

A6: now

consider x being set ;
assume A7: not y in rng f ; :: thesis: ex x being set st f " {y} c= {x}
take x = x; :: thesis: f " {y} c= {x}
rng f misses {y} by A7, ZFMISC_1:56;
then f " {y} = {} by RELAT_1:173;
hence f " {y} c= {x} by XBOOLE_1:2; :: thesis: verum

end;

now

assume y in rng f ; :: thesis: ex x being set st f " {y} c= {x}
then consider x being set such that
A8: f " {y} = {x} by A5;
take x = x; :: thesis: f " {y} c= {x}
thus f " {y} c= {x} by A8; :: thesis: verum

end;

hence ex x being set st f " {y} c= {x} by A6; :: thesis: verum

end;

hence ( f is one-to-one iff for y being set ex x being set st f " {y} c= {x} ) by Th144; :: thesis: verum