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

now

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

A1: now

A2: now

assume [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;

A5: now

assume [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;

assume [x,y] in (P * R) \/ (P * Q) ; :: thesis: [x,y] in P * (R \/ Q)
hence [x,y] in P * (R \/ Q) by A5, A2, XBOOLE_0:def 3; :: thesis: verum

end;

now

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;

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

end;

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