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

proof

let f be set ; :: according to TARSKI:def 3 :: thesis: ( not f in JUMP I or f in rng (JumpPart I) )
assume A1: f in JUMP I ; :: thesis: f in rng (JumpPart I)

per cases ( I = [0,{},{}] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo (a,b) or ex a, b being Data-Location of R st I = SubFrom (a,b) or ex a, b being Data-Location of R st I = MultBy (a,b) or ex i1 being Element of NAT st I = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:7;

suppose A2: I = [0,{},{}] ; :: thesis: f in rng (JumpPart I)

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

end;

suppose ex a, b being Data-Location of R st I = a := b ; :: thesis: f in rng (JumpPart I)

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

end;

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

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

end;

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

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

end;

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

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

end;

suppose A3: ex i1 being Element of NAT st I = goto (i1,R) ; :: thesis: f in rng (JumpPart I)

consider i1 being Element of NAT such that
A4: I = goto (i1,R) by A3;
A5: JumpPart (goto (i1,R)) = <*i1*> by RECDEF_2:def 2;
rng <*i1*> = {i1} by FINSEQ_1:39;
hence f in rng (JumpPart I) by A1, A4, A5, Th31; :: thesis: verum

end;

suppose A6: ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 ; :: thesis: f in rng (JumpPart I)

consider a being Data-Location of R, i1 being Element of NAT such that
A7: I = a =0_goto i1 by A6;
A8: JumpPart (a =0_goto i1) = <*i1*> by RECDEF_2:def 2;
rng <*i1*> = {i1} by FINSEQ_1:39;
hence f in rng (JumpPart I) by A1, A7, A8, Th34; :: thesis: verum

end;

suppose ex a being Data-Location of R ex r being Element of R st I = a := r ; :: thesis: f in rng (JumpPart I)

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

end;

end;

end;

let f be set ; :: according to TARSKI:def 3 :: thesis: ( not f in proj2 (JumpPart I) or f in JUMP I )
assume f in rng (JumpPart I) ; :: thesis: f in JUMP I
then consider k being set such that
A9: k in dom (JumpPart I) and
A10: f = (JumpPart I) . k by FUNCT_1:def 3;

per cases ( I = [0,{},{}] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo (a,b) or ex a, b being Data-Location of R st I = SubFrom (a,b) or ex a, b being Data-Location of R st I = MultBy (a,b) or ex i1 being Element of NAT st I = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:7;

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

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

end;

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

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

end;

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

then consider a, b being Data-Location of R such that
A12: I = AddTo (a,b) ;
k in dom {} by A9, A12, RECDEF_2:def 2;
hence f in JUMP I ; :: thesis: verum

end;

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

then consider a, b being Data-Location of R such that
A13: I = SubFrom (a,b) ;
k in dom {} by A9, A13, RECDEF_2:def 2;
hence f in JUMP I ; :: thesis: verum

end;

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

then consider a, b being Data-Location of R such that
A14: I = MultBy (a,b) ;
k in dom {} by A9, A14, RECDEF_2:def 2;
hence f in JUMP I ; :: thesis: verum

end;

suppose ex i1 being Element of NAT st I = goto (i1,R) ; :: thesis: f in JUMP I

then consider i1 being Element of NAT such that
A15: I = goto (i1,R) ;
A16: JumpPart I = <*i1*> by A15, RECDEF_2:def 2;
then k = 1 by A9, Lm1;
then A17: f = i1 by A16, A10, FINSEQ_1:def 8;
JUMP I = {i1} by A15, Th31;
hence f in JUMP I by A17, TARSKI:def 1; :: thesis: verum

end;

suppose ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 ; :: thesis: f in JUMP I

then consider a being Data-Location of R, i1 being Element of NAT such that
A18: I = a =0_goto i1 ;
A19: JumpPart I = <*i1*> by A18, RECDEF_2:def 2;
then k = 1 by A9, Lm1;
then A20: f = i1 by A19, A10, FINSEQ_1:40;
JUMP I = {i1} by A18, Th34;
hence f in JUMP I by A20, TARSKI:def 1; :: thesis: verum

end;

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

then consider a being Data-Location of R, r being Element of R such that
A21: I = a := r ;
k in dom {} by A9, A21, RECDEF_2:def 2;
hence f in JUMP I ; :: thesis: verum

end;

end;