let s, ss be State of SCMPDS ; :: thesis: (s +* (ss | NAT )) | SCM-Data-Loc = DataPart s
dom (ss | NAT ) = NAT by SCMPDS_6:1;
hence (s +* (ss | NAT )) | SCM-Data-Loc = DataPart s by AMI_2:29, FUNCT_4:76, SCMPDS_2:100; :: thesis: verum