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} )
assume A2: y in rng f ; :: thesis: ex x being set st f " {y} = {x}
consider x being set such that
A3: f " {y} c= {x} by A1;
take x ; :: thesis: f " {y} = {x}
consider x1 being set such that
A4: x1 in dom f and
A5: y = f . x1 by A2, Def5;
f . x1 in {y} by A5, TARSKI:def 1;
then f " {y} <> {} by A4, Def13;
hence f " {y} = {x} by A3, ZFMISC_1:39; :: thesis: verum

end;

assume A6: 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}

A7: 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 A6;
take x = x; :: thesis: f " {y} c= {x}
thus f " {y} c= {x} by A8; :: thesis: verum

end;

now

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

end;

hence ex x being set st f " {y} c= {x} by A7; :: 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