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
let x be object ; :: according to RELAT_1:def 2 :: thesis: for b being object holds
( [x,b] in (P * R) | X iff [x,b] in (P | X) * R )
let y be object ; :: thesis: ( [x,y] in (P * R) | X iff [x,y] in (P | X) * R )
hereby :: thesis: ( [x,y] in (P | X) * R implies [x,y] in (P * R) | X )
assume A1: [x,y] in (P * R) | X ; :: thesis: [x,y] in (P | X) * R
then [x,y] in P * R by Def9;
then consider a being object such that
A2: [x,a] in P and
A3: [a,y] in R by Def6;
x in X by A1, Def9;
then [x,a] in P | X by A2, Def9;
hence [x,y] in (P | X) * R by A3, Def6; :: thesis: verum
end;
assume [x,y] in (P | X) * R ; :: thesis: [x,y] in (P * R) | X
then consider a being object such that
A4: [x,a] in P | X and
A5: [a,y] in R by Def6;
[x,a] in P by A4, Def9;
then A6: [x,y] in P * R by A5, Def6;
x in X by A4, Def9;
hence [x,y] in (P * R) | X by A6, Def9; :: thesis: verum