theorem :: SCMPDS_2:13

for a being Int_position holds InsCode (return a) = 1 ;