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

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

A1: now :: thesis: ( y in rng R implies y in R .: X )

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

end;

now :: thesis: ( y in R .: X implies y in rng R )

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 XTUPLE_0:def 13; :: 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 :: thesis: for x being set holds
( x in R " Y iff x in dom R )

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

A3: now :: thesis: ( x in dom R implies x in R " Y )

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

end;

now :: thesis: ( x in R " Y implies x in dom R )

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 XTUPLE_0:def 12; :: 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