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 object 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 4 :: thesis: contradiction
A5: f " (f .: {x1}) c= {x1} by A1;
A6: Im (f,x2) = {(f . x2)} by A3, Th58;
A7: Im (f,x1) = {(f . x1)} by A2, Th58;
f . x1 in rng f by A2, Def3;
then f " (f .: {x1}) <> {} by A7, Th71;
then f " (f .: {x1}) = {x1} by A5, ZFMISC_1:33;
hence contradiction by A1, A4, A7, A6, ZFMISC_1:3; :: thesis: verum