let i be Instruction of S; :: according to COMPOS_2:def 5 :: thesis: ( i in rng (I ';' J) implies rng (JumpPart i) c= dom (I ';' J) )
assume A1: i in rng (I ';' J) ; :: thesis: rng (JumpPart i) c= dom (I ';' J)
rng (I ';' J) c= (rng (CutLastLoc I)) \/ (rng (Reloc (J,((card I) -' 1)))) by FUNCT_4:17;

per cases then ( i in rng (CutLastLoc I) or i in rng (Reloc (J,((card I) -' 1))) ) by A1, XBOOLE_0:def 3;

suppose A2: i in rng (CutLastLoc I) ; :: thesis: rng (JumpPart i) c= dom (I ';' J)

rng (CutLastLoc I) c= rng I by RELAT_1:11;
then A3: rng (JumpPart i) c= dom I by A2, Def5;
dom I c= dom (I ';' J) by COMPOS_1:21;
hence rng (JumpPart i) c= dom (I ';' J) by A3; :: thesis: verum

end;

suppose i in rng (Reloc (J,((card I) -' 1))) ; :: thesis: rng (JumpPart i) c= dom (I ';' J)

then A4: rng (JumpPart i) c= dom (Reloc (J,((card I) -' 1))) by Def5;
dom (Reloc (J,((card I) -' 1))) c= dom (I ';' J) by FUNCT_4:10;
hence rng (JumpPart i) c= dom (I ';' J) by A4; :: thesis: verum

end;

end;