let P, Q, R be Relation; (P * R) * Q = P * (R * Q)
let a be object ; RELAT_1:def 2 for b being object holds
( [a,b] in (P * R) * Q iff [a,b] in P * (R * Q) )
let b be object ; ( [a,b] in (P * R) * Q iff [a,b] in P * (R * Q) )
hereby ( [a,b] in P * (R * Q) implies [a,b] in (P * R) * Q )
assume
[a,b] in (P * R) * Q
;
[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;
verum
end;
assume
[a,b] in P * (R * Q)
; [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; verum