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 set holds
( y in f .: X iff y in (f " ) " X )

proof

let y be set ; :: 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 set such that
A2: x in dom f and
A3: x in X and
A4: y = f . x by Def12;
y in rng f by A2, A4, Def5;
then ( y in dom (f " ) & (f " ) . (f . x) = x ) by A1, A2, Th54;
hence y in (f " ) " X by A3, A4, Def13; :: thesis: verum

end;

assume y in (f " ) " X ; :: thesis: y in f .: X
then A5: ( y in dom (f " ) & (f " ) . y in X ) by Def13;
then y in rng f by A1, Th54;
then consider x being set such that
A6: x in dom f and
A7: y = f . x by Def5;
(f " ) . y = x by A1, A6, A7, Th56;
hence y in f .: X by A5, A6, A7, Def12; :: thesis: verum

end;

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