for s being State of SCMPDS
for d being Int_position holds d in dom s