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