let X be set ; for P, R being Relation holds P * (R | X) = (X |` P) * R
let P, R be Relation; P * (R | X) = (X |` P) * R
A1:
now for x being object st x in (X |` P) * R holds
x in P * (R | X)let x be
object ;
( x in (X |` P) * R implies x in P * (R | X) )assume A2:
x in (X |` P) * R
;
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;
verum end;
now for x being object st x in P * (R | X) holds
x in (X |` P) * Rlet x be
object ;
( x in P * (R | X) implies x in (X |` P) * R )assume A7:
x in P * (R | X)
;
x in (X |` P) * Rthen 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;
verum end;
hence
P * (R | X) = (X |` P) * R
by A1; verum