theorem Th8: :: SCMPDS_9:8

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