let X be set ; :: thesis: for R being Relation holds rng (R | X) = R .: X
let R be Relation; :: thesis: rng (R | X) = R .: X
for y being object holds
( y in rng (R | X) iff y in R .: X )

proof

let y be object ; :: thesis: ( y in rng (R | X) iff y in R .: X )
thus ( y in rng (R | X) implies y in R .: X ) :: thesis: ( y in R .: X implies y in rng (R | X) )

proof

assume y in rng (R | X) ; :: thesis: y in R .: X
then consider x being object such that
A1: [x,y] in R | X by XTUPLE_0:def 13;
( x in X & [x,y] in R ) by A1, Def9;
hence y in R .: X by Def11; :: thesis: verum

end;

assume y in R .: X ; :: thesis: y in rng (R | X)
then consider x being object such that
A2: ( [x,y] in R & x in X ) by Def11;
[x,y] in R | X by A2, Def9;
hence y in rng (R | X) by XTUPLE_0:def 13; :: thesis: verum

end;

hence rng (R | X) = R .: X by TARSKI:2; :: thesis: verum