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: y in Y by Def12;
A3: [x,y] in R by A1, Def12;
then x in dom R by Def4;
then [x,y] in [:(dom R),Y:] by A2, ZFMISC_1:def 2;
hence [x,y] in P by A3, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

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