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:
A2: f is one-to-one

proof

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;

A5: NAT c= rng f

proof

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 & il. i = f . i ) by A1, FUNCT_2:def 1;
hence x in rng f by FUNCT_1:def 5; :: thesis:

end;

rng f c= NAT by RELAT_1:def 19;
then NAT = rng f by A5, XBOOLE_0:def 10;
then f is onto by FUNCT_2:def 3;
hence f is bijective by A2, FUNCT_2:def 4; :: thesis:
let k be Element of NAT ; :: thesis:
A6: ( f . (k + 1) = il. (k + 1) & f . k = il. k ) by A1;
A7: SUCC (f . k) = {(f . k),(Next (f . k))} by Th64;
hence f . (k + 1) in SUCC (f . k) by A6, TARSKI:def 2; :: thesis:
let j be Element of NAT ; :: thesis:
A8: dom f = NAT by FUNCT_2:def 1;
assume A9: f . j in SUCC (f . k) ; :: thesis:

per cases by A7, A9, TARSKI:def 2;

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

hence k <= j by A2, A8, FUNCT_1:def 8; :: thesis:

end;

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

then j = k + 1 by A2, A6, A8, FUNCT_1:def 8;
hence k <= j by NAT_1:11; :: thesis:

end;

end;