theorem Th1: :: AMISTD_1:1

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for i being Element of the InstructionsF of S st ( for l being Nat holds NIC (i,l) = {l} ) holds
JUMP i is empty