theorem Th17: :: AMI_6:17

for a being Data-Location
for il, k being Nat holds NIC ((a =0_goto k),il) = {k,(il + 1)}