let s be State of ; :: thesis: dom (s | NAT ) = NAT
thus dom (s | NAT ) = (dom s) /\ NAT by RELAT_1:90
.= ((SCM-Data-Loc \/ {(IC SCMPDS )}) \/ NAT ) /\ NAT by SCMPDS_4:19
.= NAT by XBOOLE_1:21 ; :: thesis: verum