theorem Th5: :: SCMPDS_9:5

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