for a being Data-Location
for k1 being Nat holds (product" (JumpParts (InsCode (a =0_goto k1)))) . 1 = NAT