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