theorem :: SCMPDS_2:42

for s being State of SCMPDS holds dom (DataPart s) = SCM-Data-Loc