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