for l being Nat holds NIC (((f,b) := a),l) = {(l + 1)} by AMISTD_1:12;
hence JUMP ((f,b) := a) is empty by Lm1; :: thesis: verum