let x, X be set ; :: thesis: for R being Relation holds
( x in dom (R | X) iff ( x in X & x in dom R ) )
let R be Relation; :: thesis: ( x in dom (R | X) iff ( x in X & x in dom R ) )
thus ( x in dom (R | X) implies ( x in X & x in dom R ) ) :: thesis: ( x in X & x in dom R implies x in dom (R | X) )

proof

assume x in dom (R | X) ; :: thesis: ( x in X & x in dom R )
then consider y being set such that
A1: [x,y] in R | X by Def4;
( [x,y] in R & x in X ) by A1, Def11;
hence ( x in X & x in dom R ) by Def4; :: thesis: verum

end;

assume A2: x in X ; :: thesis: ( not x in dom R or x in dom (R | X) )
assume x in dom R ; :: thesis: x in dom (R | X)
then consider y being set such that
A3: [x,y] in R by Def4;
[x,y] in R | X by A2, A3, Def11;
hence x in dom (R | X) by Def4; :: thesis: verum