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

assume InsCode i = 6 ; :: thesis: dom (JumpPart i) = Seg 1

then i in { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } by Th9;

then consider J being Element of Segm 9, a being Nat such that

A1: i = [J,<*a*>,{}] and

J = 6 ;

JumpPart i = <*a*> by A1;

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

assume InsCode i = 6 ; :: thesis: dom (JumpPart i) = Seg 1

then i in { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } by Th9;

then consider J being Element of Segm 9, a being Nat such that

A1: i = [J,<*a*>,{}] and

J = 6 ;

JumpPart i = <*a*> by A1;

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