let f be Function; ( ( 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)
; 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
; FUNCT_1:def 4 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; verum