theorem Th19: :: AMI_6:19

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