let N be with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of 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 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 and
A2: for m, n being Element of NAT holds
( m <= n iff f1 . m <= f1 . n ) and
il. T,0 = f1 . 0 by Def12;
( l in NAT & rng f1 = NAT ) by A1, AMI_1:def 4, FUNCT_2:def 3;
then consider k being set such that
A3: k in dom f1 and
A4: f1 . k = l by 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, A2, A4, Def12; :: thesis: verum