for l being Element of NAT holds NIC ((a := k1),l) = {(l + 1)} by Th6;
hence JUMP (a := k1) is empty by Th2; :: thesis: verum