theorem Th33: :: SCMFSA10:33

for il, i1 being Nat holds NIC ((goto i1),il) = {i1}