theorem :: SCMRING3:28

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