let R, S, T be Relation; :: thesis: (R \/ S) * T = (R * T) \/ (S * T)
thus (R \/ S) * T = (R * T) \/ (S * T) :: thesis: verum

proof

let x be set ; :: according to RELAT_1:def 2 :: thesis: for b₁ being set holds
( ( not [x,b₁] in (R \/ S) * T or [x,b₁] in (R * T) \/ (S * T) ) & ( not [x,b₁] in (R * T) \/ (S * T) or [x,b₁] in (R \/ S) * T ) )
let y be set ; :: thesis: ( ( not [x,y] in (R \/ S) * T or [x,y] in (R * T) \/ (S * T) ) & ( not [x,y] in (R * T) \/ (S * T) or [x,y] in (R \/ S) * T ) )
thus ( [x,y] in (R \/ S) * T implies [x,y] in (R * T) \/ (S * T) ) :: thesis: ( not [x,y] in (R * T) \/ (S * T) or [x,y] in (R \/ S) * T )

proof

assume [x,y] in (R \/ S) * T ; :: thesis: [x,y] in (R * T) \/ (S * T)
then consider z being set such that
A1: ( [x,z] in R \/ S & [z,y] in T ) by RELAT_1:def 8;
( ( [x,z] in R & [z,y] in T ) or ( [x,z] in S & [z,y] in T ) ) by A1, XBOOLE_0:def 3;
then ( [x,y] in R * T or [x,y] in S * T ) by RELAT_1:def 8;
hence [x,y] in (R * T) \/ (S * T) by XBOOLE_0:def 3; :: thesis: verum

end;

thus ( [x,y] in (R * T) \/ (S * T) implies [x,y] in (R \/ S) * T ) :: thesis: verum

proof

A2: ( [x,y] in S * T & [x,y] in (R * T) \/ (S * T) implies [x,y] in (R \/ S) * T )

proof

assume [x,y] in S * T ; :: thesis: ( not [x,y] in (R * T) \/ (S * T) or [x,y] in (R \/ S) * T )
then consider z being set such that
A3: [x,z] in S and
A4: [z,y] in T by RELAT_1:def 8;
[x,z] in R \/ S by A3, XBOOLE_0:def 3;
hence ( not [x,y] in (R * T) \/ (S * T) or [x,y] in (R \/ S) * T ) by A4, RELAT_1:def 8; :: thesis: verum

end;

A5: ( [x,y] in R * T & [x,y] in (R * T) \/ (S * T) implies [x,y] in (R \/ S) * T )

proof

assume [x,y] in R * T ; :: thesis: ( not [x,y] in (R * T) \/ (S * T) or [x,y] in (R \/ S) * T )
then consider z being set such that
A6: [x,z] in R and
A7: [z,y] in T by RELAT_1:def 8;
[x,z] in R \/ S by A6, XBOOLE_0:def 3;
hence ( not [x,y] in (R * T) \/ (S * T) or [x,y] in (R \/ S) * T ) by A7, RELAT_1:def 8; :: thesis: verum

end;

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

end;

end;