let f be Function; :: thesis: ( ( for X being set holds f " (f .: X) c= X ) implies f is one-to-one )
assume A1: for X being set holds f " (f .: X) c= X ; :: thesis: f is one-to-one
given x1, x2 being set such that A2: ( x1 in dom f & x2 in dom f ) and
A3: f . x1 = f . x2 and
A4: x1 <> x2 ; :: according to FUNCT_1:def 8 :: thesis: contradiction
A5: ( Im f,x1 = {(f . x1)} & Im f,x2 = {(f . x2)} ) by A2, Th117;
then ( f .: {x1} <> {} & f .: {x2} <> {} & f . x1 in rng f & f . x2 in rng f ) by A2, Def5;
then ( f " (f .: {x1}) <> {} & f " (f .: {x2}) <> {} & f " (f .: {x1}) c= {x1} & f " (f .: {x2}) c= {x2} ) by A1, A5, Th142;
then ( f " (f .: {x1}) = {x1} & f " (f .: {x2}) = {x2} ) by ZFMISC_1:39;
hence contradiction by A3, A4, A5, ZFMISC_1:6; :: thesis: verum