set i = the No-StopCode Instruction of S;
take Load the No-StopCode Instruction of S ; :: thesis: Load the No-StopCode Instruction of S is halt-free
A1: rng (Load the No-StopCode Instruction of S) = { the No-StopCode Instruction of S} by AFINSQ_1:33;

now :: thesis: not halt S in rng (Load the No-StopCode Instruction of S)

assume halt S in rng (Load the No-StopCode Instruction of S) ; :: thesis: contradiction
then halt S = the No-StopCode Instruction of S by A1, TARSKI:def 1;
hence contradiction by COMPOS_0:def 12; :: thesis: verum

end;

hence Load the No-StopCode Instruction of S is halt-free ; :: thesis: verum