for s being State of SCMPDS holds SCM-Data-Loc c= dom s