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 object holds
( x in f " Y iff x in (f ") .: Y )

proof

let x be object ; :: 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 A2: x in f " Y ; :: thesis: x in (f ") .: Y
then A3: f . x in Y by Def7;
A4: x in dom f by A2, Def7;
then f . x in rng f by Def3;
then A5: f . x in dom (f ") by A1, Th31;
(f ") . (f . x) = x by A1, A4, Th31;
hence x in (f ") .: Y by A3, A5, Def6; :: thesis: verum

end;

assume x in (f ") .: Y ; :: thesis: x in f " Y
then consider y being object such that
A6: y in dom (f ") and
A7: y in Y and
A8: x = (f ") . y by Def6;
dom (f ") = rng f by A1, Th31;
then ( y = f . x & x in dom f ) by A1, A6, A8, Th31;
hence x in f " Y by A7, Def7; :: thesis: verum

end;

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