let Y, X be set ; :: thesis: for R being Relation holds (Y | R) | X = Y | (R | X)
let R be Relation; :: thesis: (Y | R) | X = Y | (R | X)
let x be set ; :: according to RELAT_1:def 2 :: thesis: for b being set holds
( [x,b] in (Y | R) | X iff [x,b] in Y | (R | X) )
let y be set ; :: thesis: ( [x,y] in (Y | R) | X iff [x,y] in Y | (R | X) )
A1: ( ( [x,y] in R & x in X ) iff [x,y] in R | X ) by Def11;
( [x,y] in Y | R iff ( [x,y] in R & y in Y ) ) by Def12;
hence ( [x,y] in (Y | R) | X iff [x,y] in Y | (R | X) ) by A1, Def11, Def12; :: thesis: verum