let A, B be set ; 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; for R1, R2 being Subset of [:A,B:] holds (R1 /\ R2) .:^ X = (R1 .:^ X) /\ (R2 .:^ X)
let R1, R2 be Subset of [:A,B:]; (R1 /\ R2) .:^ X = (R1 .:^ X) /\ (R2 .:^ X)
thus
(R1 /\ R2) .:^ X c= (R1 .:^ X) /\ (R2 .:^ X)
XBOOLE_0:def 10 (R1 .:^ X) /\ (R2 .:^ X) c= (R1 /\ R2) .:^ X
let y be object ; TARSKI:def 3 ( not y in (R1 .:^ X) /\ (R2 .:^ X) or y in (R1 /\ R2) .:^ X )
assume A3:
y in (R1 .:^ X) /\ (R2 .:^ X)
; 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 ;
( x in X implies y in Im ((R1 /\ R2),x) )
assume A6:
x in X
;
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;
verum
end;
hence
y in (R1 /\ R2) .:^ X
by Th25; verum