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 set holds
( y in rng (R | X) iff y in R .: X )

proof

let y be set ; :: 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 set such that
A1: [x,y] in R | X by Def5;
( x in X & [x,y] in R ) by A1, Def11;
hence y in R .: X by Def13; :: thesis: verum

end;

assume y in R .: X ; :: thesis: y in rng (R | X)
then consider x being set such that
A2: ( [x,y] in R & x in X ) by Def13;
[x,y] in R | X by A2, Def11;
hence y in rng (R | X) by Def5; :: thesis: verum

end;

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