let X, Y be set ; for R being Relation holds (Y |` R) | X = Y |` (R | X)
let R be Relation; (Y |` R) | X = Y |` (R | X)
let x be object ; RELAT_1:def 2 for b being object holds
( [x,b] in (Y |` R) | X iff [x,b] in Y |` (R | X) )
let y be object ; ( [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 Def9;
( [x,y] in Y |` R iff ( [x,y] in R & y in Y ) )
by Def10;
hence
( [x,y] in (Y |` R) | X iff [x,y] in Y |` (R | X) )
by A1, Def9, Def10; verum