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

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