theorem Th16: :: SCMFSA10:16

for i1 being Nat
for a being Int-Location holds JumpPart (a >0_goto i1) = <*i1*>