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 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
( Im f,x1 = {(f . x1)} & Im f,x2 = {(f . x2)} & {x1} \ {x2} = {x1} ) by A2, A4, Th117, ZFMISC_1:20;
then ( f .: ({x1} \ {x2}) = f .: {x1} & f . x1 in f .: {x1} & f .: ({x1} \ {x2}) = (f .: {x1}) \ (f .: {x2}) & (f .: {x1}) \ (f .: {x2}) = {} ) by A1, A3, TARSKI:def 1, XBOOLE_1:37;
hence contradiction ; :: thesis: verum