theorem Th2: :: AMISTD_1:2

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for il being Nat
for i being Instruction of S st i is halting holds
NIC (i,il) = {il}