theorem :: SCMPDS_2:15

for k1 being Integer
for a being Int_position holds InsCode (saveIC (a,k1)) = 3 ;