theorem Th6: :: SCMPDS_9:6

for a being Int_position
for l being Element of NAT
for k1 being Integer holds NIC ((a := k1),l) = {(l + 1)}