now :: thesis: for y being object st y in rng ((i,j) -cut b) holds
y in NAT

let y be object ; :: 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 object such that
A1: x in dom ((i,j) -cut b) and
A2: ((i,j) -cut b) . x = y by FUNCT_1:def 3;
A3: x in j -' i by A1;
j -' i = { k where k is Nat : k < j -' i } by AXIOMS:4;
then ex k being Nat st
( k = x & k < j -' i ) by A3;
then reconsider x = x as Element of NAT by ORDINAL1:def 12;
y = b . (i + x) by A2, A3, Def1;
hence y in NAT ; :: thesis: verum

end;

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