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