theorem :: AMI_6:12

for k1 being Nat holds (product" (JumpParts (InsCode (SCM-goto k1)))) . 1 = NAT