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

y in NAT

then
rng ((i,j) -cut b) c= NAT
;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;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

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