for k1, k2 being Integer
for a being Int_position holds InsCode (AddTo (a,k1,k2)) = 8 ;