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