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

proof

let y be object ; :: thesis: ( y in f .: X iff y in (f ") " X )
thus ( y in f .: X implies y in (f ") " X ) :: thesis: ( y in (f ") " X implies y in f .: X )

proof

assume y in f .: X ; :: thesis: y in (f ") " X
then consider x being object such that
A2: x in dom f and
A3: x in X and
A4: y = f . x by Def6;
y in rng f by A2, A4, Def3;
then A5: y in dom (f ") by A1, Th31;
(f ") . (f . x) = x by A1, A2, Th31;
hence y in (f ") " X by A3, A4, A5, Def7; :: thesis: verum

end;

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

end;

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