theorem Th35: :: SCMFSA10:35

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