let i be Element of SCM-Instr ; :: thesis: ( ( InsCode i = 7 or InsCode i = 8 ) implies dom (JumpPart i) = Seg 1 )

assume ( InsCode i = 7 or InsCode i = 8 ) ; :: thesis: dom (JumpPart i) = Seg 1

then i in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } by Th9;

then consider K being Element of Segm 9, a1 being Nat, b1 being Element of SCM-Data-Loc such that

A1: i = [K,<*a1*>,<*b1*>] and

K in {7,8} ;

JumpPart i = <*a1*> by A1;

hence dom (JumpPart i) = Seg 1 by FINSEQ_1:38; :: thesis: verum

assume ( InsCode i = 7 or InsCode i = 8 ) ; :: thesis: dom (JumpPart i) = Seg 1

then i in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } by Th9;

then consider K being Element of Segm 9, a1 being Nat, b1 being Element of SCM-Data-Loc such that

A1: i = [K,<*a1*>,<*b1*>] and

K in {7,8} ;

JumpPart i = <*a1*> by A1;

hence dom (JumpPart i) = Seg 1 by FINSEQ_1:38; :: thesis: verum