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