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 ;
w in X by ;
then A6: [w,z] in R | X by ;
[y,w] in P by ;
hence x in P * (R | X) by ; :: 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 ;
w in X by ;
then A11: [y,w] in X |` P by ;
[w,z] in R by ;
hence x in (X |` P) * R by ; :: thesis: verum
end;
hence P * (R | X) = (X |` P) * R by A1; :: thesis: verum