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) = [7,<*i1*>,<*a*>] `2_3 by Th15
.= <*i1*> by RECDEF_2:def 2 ; :: thesis: verum