for l being Element of NAT holds NIC (saveIC a,k1),l = {(succ l)} by Th11;
hence JUMP (saveIC a,k1) is empty by Th8; :: thesis: verum