let P, R, Q be Relation; :: thesis: (P * R) * Q = P * (R * Q)
let a be set ; :: according to RELAT_1:def 2 :: thesis: for b being set holds
( [a,b] in (P * R) * Q iff [a,b] in P * (R * Q) )
let b be set ; :: 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 set such that
A1: [a,y] in P * R and
A2: [y,b] in Q by Def8;
consider x being set such that
A3: [a,x] in P and
A4: [x,y] in R by A1, Def8;
[x,b] in R * Q by A2, A4, Def8;
hence [a,b] in P * (R * Q) by A3, Def8; :: thesis: verum

end;

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