let I be Instruction of (SCM R); :: according to AMISTD_2:def 2 :: thesis:
thus JUMP I c= rng (JumpPart I) :: according to AMISTD_2:def 1,XBOOLE_0:def 10 :: thesis:

proof

let f be object ; :: according to TARSKI:def 3 :: thesis:
assume A1: f in JUMP I ; :: thesis:

per cases by SCMRING2:7;

suppose A2: I = [0,{},{}] ; :: thesis:

JUMP (halt (SCM R)) is empty ;
hence f in rng (JumpPart I) by A1, A2; :: thesis:

end;

suppose ex a, b being Data-Location of R st I = a := b ; :: thesis:

hence f in rng (JumpPart I) by A1; :: thesis:

end;

suppose ex a, b being Data-Location of R st I = AddTo (a,b) ; :: thesis:

hence f in rng (JumpPart I) by A1; :: thesis:

end;

suppose ex a, b being Data-Location of R st I = SubFrom (a,b) ; :: thesis:

hence f in rng (JumpPart I) by A1; :: thesis:

end;

suppose ex a, b being Data-Location of R st I = MultBy (a,b) ; :: thesis:

hence f in rng (JumpPart I) by A1; :: thesis:

end;

suppose A3: ex i1 being Nat st I = goto (i1,R) ; :: thesis:

consider i1 being Nat such that
A4: I = goto (i1,R) by A3;
rng <*i1*> = {i1} by FINSEQ_1:39;
hence f in rng (JumpPart I) by A1, A4, Th30; :: thesis:

end;

suppose A5: ex a being Data-Location of R ex i1 being Nat st I = a =0_goto i1 ; :: thesis:

consider a being Data-Location of R, i1 being Nat such that
A6: I = a =0_goto i1 by A5;
rng <*i1*> = {i1} by FINSEQ_1:39;
hence f in rng (JumpPart I) by A1, A6, Th33; :: thesis:

end;

suppose ex a being Data-Location of R ex r being Element of R st I = a := r ; :: thesis:

hence f in rng (JumpPart I) by A1; :: thesis:

end;

end;

end;

let f be object ; :: according to TARSKI:def 3 :: thesis:
assume f in rng (JumpPart I) ; :: thesis:
then consider k being object such that
A7: k in dom (JumpPart I) and
A8: f = (JumpPart I) . k by FUNCT_1:def 3;

per cases by SCMRING2:7;

suppose I = [0,{},{}] ; :: thesis:

then I = halt (SCM R) ;
hence f in JUMP I by A7; :: thesis:

end;

suppose ex a, b being Data-Location of R st I = a := b ; :: thesis:

then consider a, b being Data-Location of R such that
A9: I = a := b ;
k in dom {} by A7, A9;
hence f in JUMP I ; :: thesis:

end;

suppose ex a, b being Data-Location of R st I = AddTo (a,b) ; :: thesis:

then consider a, b being Data-Location of R such that
A10: I = AddTo (a,b) ;
k in dom {} by A7, A10;
hence f in JUMP I ; :: thesis:

end;

suppose ex a, b being Data-Location of R st I = SubFrom (a,b) ; :: thesis:

then consider a, b being Data-Location of R such that
A11: I = SubFrom (a,b) ;
k in dom {} by A7, A11;
hence f in JUMP I ; :: thesis:

end;

suppose ex a, b being Data-Location of R st I = MultBy (a,b) ; :: thesis:

then consider a, b being Data-Location of R such that
A12: I = MultBy (a,b) ;
k in dom {} by A7, A12;
hence f in JUMP I ; :: thesis:

end;

suppose ex i1 being Nat st I = goto (i1,R) ; :: thesis:

then consider i1 being Nat such that
A13: I = goto (i1,R) ;
A14: JumpPart I = <*i1*> by A13;
then k = 1 by A7, Lm1;
then A15: f = i1 by A14, A8, FINSEQ_1:def 8;
JUMP I = {i1} by A13, Th30;
hence f in JUMP I by A15, TARSKI:def 1; :: thesis:

end;

suppose ex a being Data-Location of R ex i1 being Nat st I = a =0_goto i1 ; :: thesis:

then consider a being Data-Location of R, i1 being Nat such that
A16: I = a =0_goto i1 ;
A17: JumpPart I = <*i1*> by A16;
then k = 1 by A7, Lm1;
then A18: f = i1 by A17, A8, FINSEQ_1:40;
JUMP I = {i1} by A16, Th33;
hence f in JUMP I by A18, TARSKI:def 1; :: thesis:

end;

suppose ex a being Data-Location of R ex r being Element of R st I = a := r ; :: thesis:

then consider a being Data-Location of R, r being Element of R such that
A19: I = a := r ;
k in dom {} by A7, A19;
hence f in JUMP I ; :: thesis:

end;

end;