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