theorem :: SCMPDS_2:12

for k1 being Integer holds InsCode (goto k1) = 14 ;