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