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
A6: [a,y] in P * R and
A7: [y,b] in Q by Def8;
consider x being set such that
A8: [a,x] in P and
A9: [x,y] in R by A6, Def8;
[x,b] in R * Q by A7, A9, Def8;
hence [a,b] in P * (R * Q) by A8, 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
A2: [a,y] in P and
A3: [y,b] in R * Q by Def8;
consider x being set such that
A4: [y,x] in R and
A5: [x,b] in Q by A3, Def8;
[a,x] in P * R by A2, A4, Def8;
hence [a,b] in (P * R) * Q by A5, Def8; :: thesis: verum