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

hereby :: thesis: ( [a,b] in P * (R * Q) implies [a,b] in (P * R) * Q )

assume [a,b] in (P * R) * Q ; :: thesis: [a,b] in P * (R * Q)
then consider y being object such that
A1: [a,y] in P * R and
A2: [y,b] in Q by Def6;
consider x being object such that
A3: [a,x] in P and
A4: [x,y] in R by A1, Def6;
[x,b] in R * Q by A2, A4, Def6;
hence [a,b] in P * (R * Q) by A3, Def6; :: thesis: verum

end;

assume [a,b] in P * (R * Q) ; :: thesis: [a,b] in (P * R) * Q
then consider y being object such that
A5: [a,y] in P and
A6: [y,b] in R * Q by Def6;
consider x being object such that
A7: [y,x] in R and
A8: [x,b] in Q by A6, Def6;
[a,x] in P * R by A5, A7, Def6;
hence [a,b] in (P * R) * Q by A8, Def6; :: thesis: verum