let X, Y be set ; :: thesis: for R being Relation of X,Y holds

( ( for y being object st y in Y holds

ex x being object st [x,y] in R ) iff rng R = Y )

let R be Relation of X,Y; :: thesis: ( ( for y being object st y in Y holds

ex x being object st [x,y] in R ) iff rng R = Y )

thus ( ( for y being object st y in Y holds

ex x being object st [x,y] in R ) implies rng R = Y ) :: thesis: ( rng R = Y implies for y being object st y in Y holds

ex x being object st [x,y] in R )

ex x being object st [x,y] in R ) by XTUPLE_0:def 13; :: thesis: verum

( ( for y being object st y in Y holds

ex x being object st [x,y] in R ) iff rng R = Y )

let R be Relation of X,Y; :: thesis: ( ( for y being object st y in Y holds

ex x being object st [x,y] in R ) iff rng R = Y )

thus ( ( for y being object st y in Y holds

ex x being object st [x,y] in R ) implies rng R = Y ) :: thesis: ( rng R = Y implies for y being object st y in Y holds

ex x being object st [x,y] in R )

proof

thus
( rng R = Y implies for y being object st y in Y holds
assume A1:
for y being object st y in Y holds

ex x being object st [x,y] in R ; :: thesis: rng R = Y

end;ex x being object st [x,y] in R ; :: thesis: rng R = Y

now :: thesis: for y being object holds

( y in rng R iff y in Y )

hence
rng R = Y
by TARSKI:2; :: thesis: verum( y in rng R iff y in Y )

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

end;now :: thesis: ( y in Y implies y in rng R )

hence
( y in rng R iff y in Y )
; :: thesis: verumassume
y in Y
; :: thesis: y in rng R

then ex x being object st [x,y] in R by A1;

hence y in rng R by XTUPLE_0:def 13; :: thesis: verum

end;then ex x being object st [x,y] in R by A1;

hence y in rng R by XTUPLE_0:def 13; :: thesis: verum

ex x being object st [x,y] in R ) by XTUPLE_0:def 13; :: thesis: verum