theorem :: SCMPDS_2:25

for k1, k2 being Integer
for a, b being Int_position holds InsCode ((a,k1) := (b,k2)) = 13 ;