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