let i be Element of SCMPDS-Instr ; :: thesis: ( InsCode i = 1 implies JumpPart i = {} )
assume InsCode i = 1 ; :: thesis: JumpPart i = {}
then i in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } by Th8;
then ex sp being Element of SCM-Data-Loc st i = [1,{},<*sp*>] ;
hence JumpPart i = {} ; :: thesis: verum