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 )

proof

assume A1: for y being object st y in Y holds
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 )

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

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

assume 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;

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

end;

hence rng R = Y by TARSKI:2; :: thesis: verum

end;

thus ( rng R = Y implies for y being object st y in Y holds
ex x being object st [x,y] in R ) by XTUPLE_0:def 13; :: thesis: verum