let i be Element of SCM-Instr ; ( ( InsCode i = 7 or InsCode i = 8 ) implies dom (JumpPart i) = Seg 1 )
assume
( InsCode i = 7 or InsCode i = 8 )
; 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; verum