let X be set ; :: thesis: for P, R being Relation holds P * (R | X) = (X |` P) * R
let P, R be Relation; :: thesis: P * (R | X) = (X |` P) * R

A1: now :: thesis: for x being object st x in (X |` P) * R holds
x in P * (R | X)

let x be object ; :: thesis: ( x in (X |` P) * R implies x in P * (R | X) )
assume A2: x in (X |` P) * R ; :: thesis: x in P * (R | X)
then consider y, z being object such that
A3: x = [y,z] by RELAT_1:def 1;
consider w being object such that
A4: [y,w] in X |` P and
A5: [w,z] in R by A2, A3, RELAT_1:def 8;
w in X by A4, RELAT_1:def 12;
then A6: [w,z] in R | X by A5, RELAT_1:def 11;
[y,w] in P by A4, RELAT_1:def 12;
hence x in P * (R | X) by A3, A6, RELAT_1:def 8; :: thesis: verum

end;

now :: thesis: for x being object st x in P * (R | X) holds
x in (X |` P) * R

let x be object ; :: thesis: ( x in P * (R | X) implies x in (X |` P) * R )
assume A7: x in P * (R | X) ; :: thesis: x in (X |` P) * R
then consider y, z being object such that
A8: x = [y,z] by RELAT_1:def 1;
consider w being object such that
A9: [y,w] in P and
A10: [w,z] in R | X by A7, A8, RELAT_1:def 8;
w in X by A10, RELAT_1:def 11;
then A11: [y,w] in X |` P by A9, RELAT_1:def 12;
[w,z] in R by A10, RELAT_1:def 11;
hence x in (X |` P) * R by A8, A11, RELAT_1:def 8; :: thesis: verum

end;

hence P * (R | X) = (X |` P) * R by A1; :: thesis: verum