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