for k being Integer ex s being State of SCMPDS st
for d being Int_position holds s . d = k