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