for l being Element of NAT holds NIC ((AddTo (a,b)),l) = {(succ l)} by Th70;
hence JUMP (AddTo (a,b)) is empty by Lm6; :: thesis: verum