let Y be set ; :: thesis: for f being Function st f is one-to-one holds
f " Y = (f " ) .: Y
let f be Function; :: thesis: ( f is one-to-one implies f " Y = (f " ) .: Y )
assume A1: f is one-to-one ; :: thesis: f " Y = (f " ) .: Y
for x being set holds
( x in f " Y iff x in (f " ) .: Y )

proof

let x be set ; :: thesis: ( x in f " Y iff x in (f " ) .: Y )
thus ( x in f " Y implies x in (f " ) .: Y ) :: thesis: ( x in (f " ) .: Y implies x in f " Y )

proof

assume x in f " Y ; :: thesis: x in (f " ) .: Y
then ( x in dom f & f . x in Y ) by Def13;
then ( x in dom f & f . x in rng f & f . x in Y ) by Def5;
then ( (f " ) . (f . x) = x & f . x in dom (f " ) & f . x in Y ) by A1, Th54;
hence x in (f " ) .: Y by Def12; :: thesis: verum

end;

assume x in (f " ) .: Y ; :: thesis: x in f " Y
then consider y being set such that
A2: y in dom (f " ) and
A3: y in Y and
A4: x = (f " ) . y by Def12;
dom (f " ) = rng f by A1, Th54;
then ( y = f . x & x in dom f ) by A1, A2, A4, Th54;
hence x in f " Y by A3, Def13; :: thesis: verum

end;

hence f " Y = (f " ) .: Y by TARSKI:2; :: thesis: verum