let X1, X2 be set ; :: thesis: for f being Function st f is one-to-one holds
f .: (X1 \ X2) = (f .: X1) \ (f .: X2)
let f be Function; :: thesis: ( f is one-to-one implies f .: (X1 \ X2) = (f .: X1) \ (f .: X2) )
assume A1: f is one-to-one ; :: thesis: f .: (X1 \ X2) = (f .: X1) \ (f .: X2)
A2: f .: (X1 \ X2) c= (f .: X1) \ (f .: X2)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (X1 \ X2) or y in (f .: X1) \ (f .: X2) )
assume y in f .: (X1 \ X2) ; :: thesis: y in (f .: X1) \ (f .: X2)
then consider x being set such that
A3: x in dom f and
A4: x in X1 \ X2 and
A5: y = f . x by Def12;
A6: not x in X2 by A4, XBOOLE_0:def 5;

A7: now

assume y in f .: X2 ; :: thesis: contradiction
then ex z being set st
( z in dom f & z in X2 & y = f . z ) by Def12;
hence contradiction by A1, A3, A5, A6, Def8; :: thesis: verum

end;

y in f .: X1 by A3, A4, A5, Def12;
hence y in (f .: X1) \ (f .: X2) by A7, XBOOLE_0:def 5; :: thesis: verum

end;

(f .: X1) \ (f .: X2) c= f .: (X1 \ X2) by RELAT_1:122;
hence f .: (X1 \ X2) = (f .: X1) \ (f .: X2) by A2, XBOOLE_0:def 10; :: thesis: verum