let P, R, Q be Relation; :: thesis: P * (R \/ Q) = (P * R) \/ (P * Q)
let x be set ; :: according to RELAT_1:def 2 :: thesis: for b being set holds
( [x,b] in P * (R \/ Q) iff [x,b] in (P * R) \/ (P * Q) )
let y be set ; :: 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 set such that
A8: [x,z] in P and
A9: [z,y] in R \/ Q by Def8;
( [z,y] in R or [z,y] in Q ) by A9, XBOOLE_0:def 3;
then ( [x,y] in P * R or [x,y] in P * Q ) by A8, Def8;
hence [x,y] in (P * R) \/ (P * Q) by XBOOLE_0:def 3; :: thesis: verum

end;

assume A1: [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 A1, XBOOLE_0:def 3;

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

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

end;

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

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

end;

end;