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, y be object ; :: according to RELAT_1:def 2 :: 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 object 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;

assume A2: [x,y] in (R * T) \/ (S * T) ; :: thesis: [x,y] in (R \/ S) * T

per cases ( [x,y] in S * T or [x,y] in R * T ) by A2, XBOOLE_0:def 3;

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

then consider z being object 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 [x,y] in (R \/ S) * T by A4, RELAT_1:def 8; :: thesis: verum

end;

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

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

end;

end;

end;