for a being Int_position
for s being State of SCMPDS holds (Initialize s) . a = s . a