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