theorem :: SCMFSA10:31

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