let s be State of SCMPDS; :: thesis: dom s = {(IC )} \/ SCM-Data-Loc
dom s = the carrier of SCMPDS by PARTFUN1:def 2;
hence dom s = {(IC )} \/ SCM-Data-Loc by SCMPDS_2:84, STRUCT_0:4; :: thesis: verum