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 :: thesis: 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 ; :: thesis: ( ( 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 ) :: thesis: ( ex x being object st [x,y] in R implies y in rng f )
proof
assume y in rng f ; :: thesis: 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 ; :: thesis: [(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; :: thesis: verum
end;
given x being object such that A6: [x,y] in R ; :: thesis: y in rng f
f . [x,y] = [x,y] `2 by A2, A6
.= y ;
hence y in rng f by A1, A6, FUNCT_1:3; :: thesis: verum
end;
then rng f = rng R by XTUPLE_0:def 13;
hence rng R is finite by A1, Th8; :: thesis: verum