theorem :: SCMPDS_9:14

for a being Int_position
for l being Element of NAT
for k1, k2 being Integer holds NIC (((a,k1) <>0_goto k2),l) = {(l + 1),|.(k2 + l).|}