let P, R, Q be Relation; :: thesis: P * (R /\ Q) c= (P * R) /\ (P * Q)

now

let x, y be set ; :: thesis: ( [x,y] in P * (R /\ Q) implies [x,y] in (P * R) /\ (P * Q) )

now

assume [x,y] in P * (R /\ Q) ; :: thesis: [x,y] in (P * R) /\ (P * Q)
then consider z being set such that
A1: [x,z] in P and
A2: [z,y] in R /\ Q by Def8;
[z,y] in Q by A2, XBOOLE_0:def 4;
then A3: [x,y] in P * Q by A1, Def8;
[z,y] in R by A2, XBOOLE_0:def 4;
then [x,y] in P * R by A1, Def8;
hence [x,y] in (P * R) /\ (P * Q) by A3, XBOOLE_0:def 4; :: thesis: verum

end;

hence ( [x,y] in P * (R /\ Q) implies [x,y] in (P * R) /\ (P * Q) ) ; :: thesis: verum

end;

hence P * (R /\ Q) c= (P * R) /\ (P * Q) by Def3; :: thesis: verum