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