let f be Function; :: thesis: ( ( for X1, X2 being set holds f .: (X1 \ X2) = (f .: X1) \ (f .: X2) ) implies f is one-to-one )
assume A1: for X1, X2 being set holds f .: (X1 \ X2) = (f .: X1) \ (f .: X2) ; :: thesis: f is one-to-one
given x1, x2 being object 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 4 :: thesis: contradiction
A5: f .: ({x1} \ {x2}) = f .: {x1} by A4, ZFMISC_1:14;
A6: f .: ({x1} \ {x2}) = (f .: {x1}) \ (f .: {x2}) by A1;
( Im (f,x1) = {(f . x1)} & Im (f,x2) = {(f . x2)} ) by A2, Th58;
hence contradiction by A3, A5, A6, XBOOLE_1:37; :: thesis: verum