theorem :: SCMFSA_2:23

for lb being Nat holds InsCode (goto lb) = 6 ;