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