let R be good Ring; :: thesis:
let f be IL-Function of NAT , SCM R; :: thesis:
assume A1: for k being Element of NAT holds f . k = il. k ; :: thesis:
thus A2: f is bijective :: thesis:

thus f is one-to-one :: according to FUNCT_2:def 4 :: thesis:

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis:
assume that
A3: ( x1 in dom f & x2 in dom f ) and
A4: f . x1 = f . x2 ; :: thesis:
reconsider k1 = x1, k2 = x2 as Element of NAT by A3, FUNCT_2:def 1;
( f . k1 = il. k1 & f . k2 = il. k2 ) by A1;
hence x1 = x2 by A4; :: thesis:

end;

thus f is onto :: thesis:

thus rng f c= NAT by RELSET_1:12; :: according to FUNCT_2:def 3,XBOOLE_0:def 10 :: thesis:
thus NAT c= rng f :: thesis:

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in NAT ; :: thesis:
then reconsider l = x as Instruction-Location of SCM by AMI_1:def 4;
reconsider i = l as Element of NAT by ORDINAL1:def 13;
dom f = NAT by FUNCT_2:def 1;
then ( il. i = f . i & i in dom f ) by A1;
hence x in rng f by FUNCT_1:def 5; :: thesis:

end;

let k be Element of NAT ; :: thesis:
A6: SUCC (f . k) = {(f . k),(Next (f . k))} by Th64;
A7: ( f . (k + 1) = il. (k + 1) & f . k = il. k ) by A1;
thus f . (k + 1) in SUCC (f . k) by A6, A7, TARSKI:def 2; :: thesis:
let j be Element of NAT ; :: thesis:
assume A11: f . j in SUCC (f . k) ; :: thesis:
A12: f is one-to-one by A2, FUNCT_2:def 4;
A13: dom f = NAT by FUNCT_2:def 1;

per cases by A6, A11, TARSKI:def 2;

suppose f . j = f . k ; :: thesis:

hence k <= j by A12, A13, FUNCT_1:def 8; :: thesis:

end;

suppose f . j = Next (f . k) ; :: thesis:

then j = k + 1 by A7, A12, A13, FUNCT_1:def 8;
hence k <= j by NAT_1:11; :: thesis:

end;