let i1 be Element of NAT ; :: thesis: for a being Int-Location holds JumpPart (a >0_goto i1) = <*i1*>
let a be Int-Location ; :: thesis: JumpPart (a >0_goto i1) = <*i1*>
thus JumpPart (a >0_goto i1) = [8,<*i1*>,<*a*>] `2_3 by Th16
.= <*i1*> by RECDEF_2:def 2 ; :: thesis: verum