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 )

( 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 object holds

( y in R .: X iff y in rng R )

hence
R .: X = rng R
by TARSKI:2; :: thesis: R " Y = dom R( y in R .: X iff y in rng R )

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

end;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 object 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;then consider x being object 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

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

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

then ex x being object 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;then ex x being object 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

now :: thesis: for x being object holds

( x in R " Y iff x in dom R )

hence
R " Y = dom R
by TARSKI:2; :: thesis: verum( x in R " Y iff x in dom R )

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

end;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 object 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;then consider y being object 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

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

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

then ex y being object 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;then ex y being object 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