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