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

now

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

proof

assume x in rng f ; :: thesis: ex y being set st [x,y] in R
then consider a being set such that
A3: a in dom f and
A4: f . a = x by FUNCT_1:def 3;
take a `2 ; :: thesis: [x,(a `2)] in R
A5: ex x, y being set st a = [x,y] by A1, A3, RELAT_1:def 1;
x = a `1 by A1, A2, A3, A4;
hence [x,(a `2)] in R by A1, A3, A5, MCART_1:8; :: thesis: verum

end;

given y being set such that A6: [x,y] in R ; :: thesis: x in rng f
f . [x,y] = [x,y] `1 by A2, A6
.= x by MCART_1:7 ;
hence x in rng f by A1, A6, FUNCT_1:3; :: thesis: verum

end;

then rng f = dom R by RELAT_1:def 4;
hence dom R is finite by A1, Th26; :: thesis: verum