let i be Element of SCM+FSA-Instr ; :: thesis: ( ( InsCode i = 9 or InsCode i = 10 ) implies JumpPart i = {} )
assume ( InsCode i = 9 or InsCode i = 10 ) ; :: thesis: JumpPart i = {}
then i in { [J,{},<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } by Th7;
then ex J being Element of Segm 13 ex c, b 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 = {} by RECDEF_2:def 2; :: thesis: verum