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

now

let x, y be set ; :: thesis: ( [x,y] in (P * R) | X iff [x,y] in (P | X) * R )

A1: now

assume [x,y] in (P | X) * R ; :: thesis: [x,y] in (P * R) | X
then consider a being set such that
A2: [x,a] in P | X and
A3: [a,y] in R by Def8;
[x,a] in P by A2, Def11;
then A4: [x,y] in P * R by A3, Def8;
x in X by A2, Def11;
hence [x,y] in (P * R) | X by A4, Def11; :: thesis: verum

end;

now

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

end;

hence ( [x,y] in (P * R) | X iff [x,y] in (P | X) * R ) by A1; :: thesis: verum

end;

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