for l being Element of NAT holds NIC ((a := k1),l) = {(succ l)} by Th12;
hence JUMP (a := k1) is empty by Th8; :: thesis: verum