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 and
A3: x2 in dom f and
A4: ( f . x1 = f . x2 & x1 <> x2 ) ; :: according to FUNCT_1:def 8 :: thesis: contradiction
A5: f " (f .: {x1}) c= {x1} by A1;
A6: Im f,x2 = {(f . x2)} by A3, Th117;
A7: Im f,x1 = {(f . x1)} by A2, Th117;
f . x1 in rng f by A2, Def5;
then f " (f .: {x1}) <> {} by A7, Th142;
then f " (f .: {x1}) = {x1} by A5, ZFMISC_1:39;
hence contradiction by A1, A4, A7, A6, ZFMISC_1:6; :: thesis: verum