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
A5: ( Im f,x1 = {(f . x1)} & Im f,x2 = {(f . x2)} & {x1} misses {x2} ) by A2, A4, Th117, ZFMISC_1:17;
then {x1} /\ {x2} = {} by XBOOLE_0:def 7;
then ( f .: ({x1} /\ {x2}) = {} & f . x1 in f .: {x1} & f .: ({x1} /\ {x2}) = (f .: {x1}) /\ (f .: {x2}) & (f .: {x1}) /\ (f .: {x2}) = f .: {x1} ) by A1, A3, A5, RELAT_1:149, TARSKI:def 1;
hence contradiction ; :: thesis: verum