let X be set ; :: thesis: for P, Q being Relation holds (P \/ Q) | X = (P | X) \/ (Q | X)
let P, Q be Relation; :: thesis: (P \/ Q) | X = (P | X) \/ (Q | X)
set R1 = P | X;
set R2 = Q | X;
set R = P \/ Q;
set LH = (P \/ Q) | X;
set RH = (P | X) \/ (Q | X);
( (P null Q) | X c= (P \/ Q) | X & (Q null P) | X c= (P \/ Q) | X ) by RELAT_1:76;
then B0: (P | X) \/ (Q | X) c= (P \/ Q) | X by XBOOLE_1:8;

now

let z be set ; :: thesis: ( z in (P \/ Q) | X implies z in (P | X) \/ (Q | X) )
assume C1: z in (P \/ Q) | X ; :: thesis: z in (P | X) \/ (Q | X)
then consider x, y being set such that
C2: z = [x,y] by RELAT_1:def 1;
C0: ( x in X & [x,y] in P \/ Q ) by C1, C2, RELAT_1:def 11;
( ( x in X & [x,y] in P ) or ( x in X & [x,y] in Q ) ) by C0, XBOOLE_0:def 3;
then ( [x,y] in P | X or [x,y] in Q | X ) by RELAT_1:def 11;
hence z in (P | X) \/ (Q | X) by C2, XBOOLE_0:def 3; :: thesis: verum

end;

then (P \/ Q) | X c= (P | X) \/ (Q | X) by TARSKI:def 3;
hence (P \/ Q) | X = (P | X) \/ (Q | X) by B0, XBOOLE_0:def 10; :: thesis: verum