consider f being Function such that
A1:
dom f = R
and
A2:
for x being object st x in R holds
f . x = x `2
from FUNCT_1:sch 3();
now for y being object holds
( ( y in rng f implies ex x being object st [x,y] in R ) & ( ex x being object st [x,y] in R implies y in rng f ) )let y be
object ;
( ( y in rng f implies ex x being object st [x,y] in R ) & ( ex x being object st [x,y] in R implies y in rng f ) )thus
(
y in rng f implies ex
x being
object st
[x,y] in R )
( ex x being object st [x,y] in R implies y in rng f )proof
assume
y in rng f
;
ex x being object st [x,y] in R
then consider a being
object such that A3:
a in dom f
and A4:
f . a = y
by FUNCT_1:def 3;
take
a `1
;
[(a `1),y] in R
A5:
ex
x,
y being
object st
a = [x,y]
by A1, A3, RELAT_1:def 1;
y = a `2
by A1, A2, A3, A4;
hence
[(a `1),y] in R
by A1, A3, A5;
verum
end; given x being
object such that A6:
[x,y] in R
;
y in rng ff . [x,y] =
[x,y] `2
by A2, A6
.=
y
;
hence
y in rng f
by A1, A6, FUNCT_1:3;
verum end;
then
rng f = rng R
by XTUPLE_0:def 13;
hence
rng R is finite
by A1, Th8; verum