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