for k1 being Integer
for a being Int_position holds InsCode (a := k1) = 2 ;