now

let y be set ; :: thesis: ( y in rng (i,j -cut b) implies y in NAT )
assume y in rng (i,j -cut b) ; :: thesis: y in NAT
then consider x being set such that
A1: x in dom (i,j -cut b) and
A2: (i,j -cut b) . x = y by FUNCT_1:def 5;
A3: x in j -' i by A1, PARTFUN1:def 4;
j -' i = { k where k is Element of NAT : k < j -' i } by AXIOMS:30;
then ex k being Element of NAT st
( k = x & k < j -' i ) by A3;
then reconsider x = x as Element of NAT ;
y = b . (i + x) by A2, A3, Def1;
hence y in NAT ; :: thesis: verum

end;

then rng (i,j -cut b) c= NAT by TARSKI:def 3;
hence i,j -cut b is natural-valued by VALUED_0:def 6; :: thesis: verum