let P, Q, R be Relation; :: thesis: P * (R \/ Q) = (P * R) \/ (P * Q)
let x be object ; :: according to RELAT_1:def 2 :: thesis: for b being object holds
( [x,b] in P * (R \/ Q) iff [x,b] in (P * R) \/ (P * Q) )
let y be object ; :: thesis: ( [x,y] in P * (R \/ Q) iff [x,y] in (P * R) \/ (P * Q) )

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

assume [x,y] in P * (R \/ Q) ; :: thesis: [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 R or [z,y] in Q ) by A2, XBOOLE_0:def 3;
then ( [x,y] in P * R or [x,y] in P * Q ) by A1, Def6;
hence [x,y] in (P * R) \/ (P * Q) by XBOOLE_0:def 3; :: thesis: verum

end;

assume A3: [x,y] in (P * R) \/ (P * Q) ; :: thesis: [x,y] in P * (R \/ Q)

per cases ( [x,y] in P * Q or [x,y] in P * R ) by A3, XBOOLE_0:def 3;

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

then consider z being object such that
A4: [x,z] in P and
A5: [z,y] in Q by Def6;
[z,y] in R \/ Q by A5, XBOOLE_0:def 3;
hence [x,y] in P * (R \/ Q) by A4, Def6; :: thesis: verum

end;

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

then consider z being object such that
A6: [x,z] in P and
A7: [z,y] in R by Def6;
[z,y] in R \/ Q by A7, XBOOLE_0:def 3;
hence [x,y] in P * (R \/ Q) by A6, Def6; :: thesis: verum

end;

end;