theorem Th9: :: SCMPDS_9:9

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