A1: rng (Load i) = {i} by AFINSQ_1:33;

now :: thesis: not halt S in rng (Load i)

assume halt S in rng (Load i) ; :: thesis: contradiction
then halt S = i by A1, TARSKI:def 1;
hence contradiction by COMPOS_0:def 12; :: thesis: verum

end;

hence Load i is halt-free ; :: thesis: verum