for N being with_zero set
for l being Nat
for i being Element of the InstructionsF of (STC N) st InsCode i = 1 holds
NIC (i,l) = {(l + 1)} by Lm4;