let s be State of SCMPDS; :: thesis: dom (DataPart s) = SCM-Data-Loc
SCM-Data-Loc c= dom s by Th50;
hence dom (DataPart s) = SCM-Data-Loc by Lm10, RELAT_1:62; :: thesis: verum