theorem :: SCMRING3:33

for R being non trivial Ring
for a being Data-Location of R
for il, i1 being Element of NAT holds NIC ((a =0_goto i1),il) = {i1,(il + 1)}