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 Z: 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 Z, XBOOLE_0:def 3;

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

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

end;

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

then A: 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 A, XBOOLE_1:1; :: thesis: verum

end;

end;