now

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