consider f being Function such that
W1: dom f = R and
W2: for x being set st x in R holds
f . x = x `2 from FUNCT_1:sch 3();

now

let y be set ; :: thesis: ( ( y in rng f implies ex x being set st [x,y] in R ) & ( ex x being set st [x,y] in R implies y in rng f ) )
thus ( y in rng f implies ex x being set st [x,y] in R ) :: thesis: ( ex x being set st [x,y] in R implies y in rng f )

proof

assume y in rng f ; :: thesis: ex x being set st [x,y] in R
then consider a being set such that
W3: a in dom f and
W4: f . a = y by FUNCT_1:def 5;
take a `1 ; :: thesis: [(a `1 ),y] in R
F: ex x, y being set st a = [x,y] by W1, W3, RELAT_1:def 1;
y = a `2 by W2, W3, W4, W1;
hence [(a `1 ),y] in R by W1, W3, F, MCART_1:8; :: thesis: verum

end;

given x being set such that G: [x,y] in R ; :: thesis: y in rng f
f . [x,y] = [x,y] `2 by W2, G
.= y by MCART_1:7 ;
hence y in rng f by W1, G, FUNCT_1:12; :: thesis: verum

end;

then rng f = rng R by RELAT_1:def 5;
hence rng R is finite by W1, Th26; :: thesis: verum