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 Z: 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 Z, TARSKI:def 1;
then rng (JumpPart i) = {} ;
hence rng (JumpPart i) c= dom (Stop S) by XBOOLE_1:2; :: thesis: verum