rng (Stop S) = {(halt S)} by AFINSQ_1:36;
hence halt S in rng (Stop S) by TARSKI:def 1; :: according to COMPOS_1:def 7 :: thesis: verum