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)
for x, y being set holds
( [x,y] in (Y | R) | X iff [x,y] in Y | (R | X) )

proof

let x, y be set ; :: thesis: ( [x,y] in (Y | R) | X iff [x,y] in Y | (R | X) )
( ( [x,y] in Y | R implies ( [x,y] in R & y in Y ) ) & ( [x,y] in R & y in Y implies [x,y] in Y | R ) & ( [x,y] in R & x in X implies [x,y] in R | X ) & ( [x,y] in R | X implies ( [x,y] in R & x in X ) ) & ( [x,y] in (Y | R) | X implies ( x in X & [x,y] in Y | R ) ) & ( x in X & [x,y] in Y | R implies [x,y] in (Y | R) | X ) & ( [x,y] in Y | (R | X) implies ( y in Y & [x,y] in R | X ) ) & ( y in Y & [x,y] in R | X implies [x,y] in Y | (R | X) ) ) by Def11, Def12;
hence ( [x,y] in (Y | R) | X iff [x,y] in Y | (R | X) ) ; :: thesis: verum

end;

hence (Y | R) | X = Y | (R | X) by Def2; :: thesis: verum