let i be Element of SCMPDS-Instr ; :: thesis: ( InsCode i = 0 implies JumpPart i = {} )
assume InsCode i = 0 ; :: thesis: JumpPart i = {}
then i in {[0,{},{}]} by Th8;
then i = [0,{},{}] by TARSKI:def 1;
hence JumpPart i = {} ; :: thesis: verum