:: deftheorem defines AddTo SCMPDS_2:def 13 :
for a, b being Int_position
for k1, k2 being Integer holds AddTo (a,k1,b,k2) = [9,{},<*a,b,k1,k2*>];