theorem Th3: :: SCMPDS_9:3

for l being Element of NAT
for k being Integer holds NIC ((goto k),l) = {|.(k + l).|}