let k be natural number ; :: thesis: il. SCM+FSA ,k = insloc k
deffunc H₁( Element of NAT ) -> Instruction-Location of SCM+FSA = insloc $1;
A1: for k being Element of NAT holds H₁(k) is Element of NAT ;
consider f being Function of NAT ,NAT such that
A2: for k being Element of NAT holds f . k = H₁(k) from FUNCT_2:sch 9(A1);
reconsider f = f as IL-Function of NAT , SCM+FSA by AMI_1:def 36;
A3: f is bijective by A2, Th85;
A4: for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k) & ( for j being Element of NAT st f . j in SUCC (f . k) holds
k <= j ) ) by A2, Th85;
ex f being IL-Function of NAT , SCM+FSA st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) & insloc k = f . k )

proof

take f ; :: thesis: ( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) & insloc k = f . k )
thus f is bijective by A2, Th85; :: thesis: ( ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) ) & insloc k = f . k )
thus for m, n being Element of NAT holds
( m <= n iff f . m <= f . n ) by A3, A4, AMISTD_1:18; :: thesis: insloc k = f . k
insloc k in NAT by AMI_1:def 4;
hence insloc k = f . k by A2; :: thesis: verum

end;

hence il. SCM+FSA ,k = insloc k by AMISTD_1:def 12; :: thesis: verum