let X be set ; :: thesis: for f being Function st f is one-to-one holds
f " (f .: X) c= X
let f be Function; :: thesis: ( f is one-to-one implies f " (f .: X) c= X )
assume A1: f is one-to-one ; :: thesis: f " (f .: X) c= X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in f " (f .: X) or x in X )
assume A2: x in f " (f .: X) ; :: thesis: x in X
then f . x in f .: X by Def13;
then A3: ex z being set st
( z in dom f & z in X & f . x = f . z ) by Def12;
x in dom f by A2, Def13;
hence x in X by A1, A3, Def8; :: thesis: verum