let S be non empty 1-sorted ; :: thesis: for i being Element of SCM-Instr S st InsCode i = 5 holds
JumpPart i = {}
let i be Element of SCM-Instr S; :: thesis: ( InsCode i = 5 implies JumpPart i = {} )
assume InsCode i = 5 ; :: thesis: JumpPart i = {}
then i in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } by Th7;
then ex a being Element of SCM-Data-Loc ex r being Element of S st i = [5,{},<*a,r*>] ;
hence JumpPart i = {} ; :: thesis: verum