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