l + k in NAT by ORDINAL1:def 13;
hence l + k is Instruction-Location of S by AMI_1:def 4; :: thesis: verum