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 Lm9, RELAT_1:91; :: thesis: verum