let X, Y be set ; :: thesis: for R being Relation of X,Y holds
( R .: X = rng R & R " Y = dom R )
let R be Relation of X,Y; :: thesis: ( R .: X = rng R & R " Y = dom R )

now

let y be set ; :: thesis: ( y in R .: X iff y in rng R )

A1: now

assume y in rng R ; :: thesis: y in R .: X
then consider x being set such that
A2: [x,y] in R by RELAT_1:def 5;
x in X by A2, ZFMISC_1:87;
hence y in R .: X by A2, RELAT_1:def 13; :: thesis: verum

end;

now

assume y in R .: X ; :: thesis: y in rng R
then ex x being set st
( [x,y] in R & x in X ) by RELAT_1:def 13;
hence y in rng R by RELAT_1:6; :: thesis: verum

end;

hence ( y in R .: X iff y in rng R ) by A1; :: thesis: verum

end;

hence R .: X = rng R by TARSKI:1; :: thesis: R " Y = dom R

now

let x be set ; :: thesis: ( x in R " Y iff x in dom R )

A3: now

assume x in dom R ; :: thesis: x in R " Y
then consider y being set such that
A4: [x,y] in R by RELAT_1:def 4;
y in Y by A4, ZFMISC_1:87;
hence x in R " Y by A4, RELAT_1:def 14; :: thesis: verum

end;

now

assume x in R " Y ; :: thesis: x in dom R
then ex y being set st
( [x,y] in R & y in Y ) by RELAT_1:def 14;
hence x in dom R by RELAT_1:6; :: thesis: verum

end;

hence ( x in R " Y iff x in dom R ) by A3; :: thesis: verum

end;

hence R " Y = dom R by TARSKI:1; :: thesis: verum