reconsider k = k as Element of NAT by ORDINAL1:def 13;
k in NAT ;
hence k is Instruction-Location of SCM by AMI_1:def 4; :: thesis: verum