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