theorem :: SCMRING3:11

for R being Ring
for a being Data-Location of R
for i1 being Nat holds InsCode (a =0_goto i1) = 7 ;