theorem :: SCMFSA10:30

for i1 being Nat holds (product" (JumpParts (InsCode (goto i1)))) . 1 = NAT