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