let P, Q, R be Relation; P * (R /\ Q) c= (P * R) /\ (P * Q)
let x be object ; RELAT_1:def 3 for b being object st [x,b] in P * (R /\ Q) holds
[x,b] in (P * R) /\ (P * Q)
let y be object ; ( [x,y] in P * (R /\ Q) implies [x,y] in (P * R) /\ (P * Q) )
assume
[x,y] in P * (R /\ Q)
; [x,y] in (P * R) /\ (P * Q)
then consider z being object such that
A1:
[x,z] in P
and
A2:
[z,y] in R /\ Q
by Def6;
[z,y] in Q
by A2, XBOOLE_0:def 4;
then A3:
[x,y] in P * Q
by A1, Def6;
[z,y] in R
by A2, XBOOLE_0:def 4;
then
[x,y] in P * R
by A1, Def6;
hence
[x,y] in (P * R) /\ (P * Q)
by A3, XBOOLE_0:def 4; verum