let R be Ring; :: thesis: for I being Element of SCM-Instr R st InsCode I = 7 holds
dom (JumpPart I) = Seg 1
let I be Element of SCM-Instr R; :: thesis: ( InsCode I = 7 implies dom (JumpPart I) = Seg 1 )
assume InsCode I = 7 ; :: thesis: dom (JumpPart I) = Seg 1
then I in { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } by Th7;
then consider i being Nat, a being Element of SCM-Data-Loc such that
A1: I = [7,<*i*>,<*a*>] ;
JumpPart I = <*i*> by A1;
hence dom (JumpPart I) = Seg 1 by FINSEQ_1:38; :: thesis: verum