let Y be set ; :: thesis: for R being Relation holds Y | R = R /\ [:(dom R),Y:]
let R be Relation; :: thesis: Y | R = R /\ [:(dom R),Y:]
reconsider P = R /\ [:(dom R),Y:] as Relation ;
for x, y being set holds
( [x,y] in Y | R iff [x,y] in P )

proof

let x, y be set ; :: thesis: ( [x,y] in Y | R iff [x,y] in P )
thus ( [x,y] in Y | R implies [x,y] in P ) :: thesis: ( [x,y] in P implies [x,y] in Y | R )

proof

assume A1: [x,y] in Y | R ; :: thesis: [x,y] in P
then A2: [x,y] in R by Def12;
then ( x in dom R & y in Y ) by A1, Def4, Def12;
then [x,y] in [:(dom R),Y:] by ZFMISC_1:def 2;
hence [x,y] in P by A2, XBOOLE_0:def 4; :: thesis: verum

end;

assume A3: [x,y] in P ; :: thesis: [x,y] in Y | R
then [x,y] in [:(dom R),Y:] by XBOOLE_0:def 4;
then ( y in Y & [x,y] in R ) by A3, XBOOLE_0:def 4, ZFMISC_1:106;
hence [x,y] in Y | R by Def12; :: thesis: verum

end;

hence Y | R = R /\ [:(dom R),Y:] by Def2; :: thesis: verum