let s be State of SCMPDS ; :: thesis: SCM-Data-Loc c= dom s
dom s = the carrier of SCMPDS by PARTFUN1:def 4;
hence SCM-Data-Loc c= dom s ; :: thesis: verum