let N be with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for l being Instruction-Location of T ex k being natural number st l = il. T,k
let T be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for l being Instruction-Location of T ex k being natural number st l = il. T,k
let l be Instruction-Location of T; :: thesis: ex k being natural number st l = il. T,k
consider f1 being IL-Function of NAT ,T such that
A1: ( f1 is bijective & ( for m, n being Element of NAT holds
( m <= n iff f1 . m <= f1 . n ) ) & il. T,0 = f1 . 0 ) by Def12;
A2: l in NAT by AMI_1:def 4;
f1 is onto by A1;
then rng f1 = NAT by FUNCT_2:def 3;
then consider k being set such that
A3: ( k in dom f1 & f1 . k = l ) by A2, FUNCT_1:def 5;
reconsider k = k as Element of NAT by A3;
take k ; :: thesis: l = il. T,k
thus l = il. T,k by A1, A3, Def12; :: thesis: verum