let i be Element of SCM+FSA-Instr ; ( ( InsCode i = 9 or InsCode i = 10 ) implies JumpPart i = {} )
assume A1:
( InsCode i = 9 or InsCode i = 10 )
; JumpPart i = {}
then
not InsCode i = 0 & ... & not InsCode i = 8
;
then
i in { [J,{},<*c,f,b*>] where J is Element of Segm 13, b, c is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} }
by A1, Th7;
then
ex J being Element of Segm 13 ex b, c being Element of SCM-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( i = [J,{},<*c,f,b*>] & J in {9,10} )
;
hence
JumpPart i = {}
; verum