let A, B be set ; :: thesis: for X being Subset of A
for R1, R2 being Subset of [:A,B:] holds (R1 /\ R2) .:^ X = (R1 .:^ X) /\ (R2 .:^ X)
let X be Subset of A; :: thesis: for R1, R2 being Subset of [:A,B:] holds (R1 /\ R2) .:^ X = (R1 .:^ X) /\ (R2 .:^ X)
let R1, R2 be Subset of [:A,B:]; :: thesis: (R1 /\ R2) .:^ X = (R1 .:^ X) /\ (R2 .:^ X)
thus (R1 /\ R2) .:^ X c= (R1 .:^ X) /\ (R2 .:^ X) :: according to XBOOLE_0:def 10 :: thesis: (R1 .:^ X) /\ (R2 .:^ X) c= (R1 /\ R2) .:^ X

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (R1 /\ R2) .:^ X or y in (R1 .:^ X) /\ (R2 .:^ X) )
assume A1: y in (R1 /\ R2) .:^ X ; :: thesis: y in (R1 .:^ X) /\ (R2 .:^ X)
then reconsider B = B as non empty set ;
reconsider y = y as Element of B by A1;
for x being set st x in X holds
y in Im (R1,x)

proof

let x be set ; :: thesis: ( x in X implies y in Im (R1,x) )
assume x in X ; :: thesis: y in Im (R1,x)
then y in Im ((R1 /\ R2),x) by A1, Th24;
then y in (Im (R1,x)) /\ (Im (R2,x)) by Th11;
hence y in Im (R1,x) by XBOOLE_0:def 4; :: thesis: verum

end;

then A2: y in R1 .:^ X by Th25;
for x being set st x in X holds
y in Im (R2,x)

proof

let x be set ; :: thesis: ( x in X implies y in Im (R2,x) )
assume x in X ; :: thesis: y in Im (R2,x)
then y in Im ((R1 /\ R2),x) by A1, Th24;
then y in (Im (R1,x)) /\ (Im (R2,x)) by Th11;
hence y in Im (R2,x) by XBOOLE_0:def 4; :: thesis: verum

end;

then y in R2 .:^ X by Th25;
hence y in (R1 .:^ X) /\ (R2 .:^ X) by A2, XBOOLE_0:def 4; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (R1 .:^ X) /\ (R2 .:^ X) or y in (R1 /\ R2) .:^ X )
assume A3: y in (R1 .:^ X) /\ (R2 .:^ X) ; :: thesis: y in (R1 /\ R2) .:^ X
then A4: y in R1 .:^ X by XBOOLE_0:def 4;
A5: y in R2 .:^ X by A3, XBOOLE_0:def 4;
reconsider B = B as non empty set by A3;
reconsider y = y as Element of B by A3;
for x being set st x in X holds
y in Im ((R1 /\ R2),x)

proof

let x be set ; :: thesis: ( x in X implies y in Im ((R1 /\ R2),x) )
assume A6: x in X ; :: thesis: y in Im ((R1 /\ R2),x)
then A7: y in Im (R1,x) by A4, Th25;
y in Im (R2,x) by A5, A6, Th25;
then y in (Im (R1,x)) /\ (Im (R2,x)) by A7, XBOOLE_0:def 4;
hence y in Im ((R1 /\ R2),x) by Th11; :: thesis: verum

end;

hence y in (R1 /\ R2) .:^ X by Th25; :: thesis: verum