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) /\ (f .: X2) c= f .: (X1 /\ X2)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (f .: X1) /\ (f .: X2) or y in f .: (X1 /\ X2) )
assume A3: y in (f .: X1) /\ (f .: X2) ; :: thesis: y in f .: (X1 /\ X2)
then y in f .: X1 by XBOOLE_0:def 4;
then consider x1 being set such that
A4: x1 in dom f and
A5: x1 in X1 and
A6: y = f . x1 by Def12;
y in f .: X2 by A3, XBOOLE_0:def 4;
then consider x2 being set such that
A7: x2 in dom f and
A8: x2 in X2 and
A9: y = f . x2 by Def12;
x1 = x2 by A1, A4, A6, A7, A9, Def8;
then x1 in X1 /\ X2 by A5, A8, XBOOLE_0:def 4;
hence y in f .: (X1 /\ X2) by A4, A6, Def12; :: thesis: verum

end;

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