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

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)

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;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

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

x in (X |` P) * R

hence
P * (R | X) = (X |` P) * R
by A1; :: thesis: verumx 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;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