let i be Instruction of S; :: according to COMPOS_2:def 5 :: thesis: ( i in rng (Stop S) implies rng (JumpPart i) c= dom (Stop S) )
assume A1: i in rng (Stop S) ; :: thesis: rng (JumpPart i) c= dom (Stop S)
rng (Stop S) = {(halt S)} by AFINSQ_1:33;
then i = halt S by A1, TARSKI:def 1;
then rng (JumpPart i) = {} ;
hence rng (JumpPart i) c= dom (Stop S) ; :: thesis: verum