let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for p being PartState of S holds (dom (NPP p)) /\ (Data-Locations S) = dom (DataPart p)
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N; :: thesis: for p being PartState of S holds (dom (NPP p)) /\ (Data-Locations S) = dom (DataPart p)
let p be PartState of S; :: thesis: (dom (NPP p)) /\ (Data-Locations S) = dom (DataPart p)
A1: dom (NPP p) c= {(IC )} \/ (dom (DataPart p)) by Th171;
not IC in Data-Locations S by Th56;
then A2: {(IC )} misses Data-Locations S by ZFMISC_1:56;
A3: ({(IC )} \/ (dom (DataPart p))) /\ (Data-Locations S) = ({(IC )} /\ (Data-Locations S)) \/ ((dom (DataPart p)) /\ (Data-Locations S)) by XBOOLE_1:23
.= {} \/ ((dom (DataPart p)) /\ (Data-Locations S)) by A2, XBOOLE_0:def 7
.= (dom (DataPart p)) /\ (Data-Locations S)
.= dom ((DataPart p) | (Data-Locations S)) by RELAT_1:90
.= dom (DataPart p) by RELAT_1:101 ;
DataPart p c= NPP p by Th169;
then A4: dom (DataPart p) c= dom (NPP p) by RELAT_1:25;
thus (dom (NPP p)) /\ (Data-Locations S) = ((dom (NPP p)) /\ ({(IC )} \/ (dom (DataPart p)))) /\ (Data-Locations S) by A1, XBOOLE_1:28
.= (dom (NPP p)) /\ (({(IC )} \/ (dom (DataPart p))) /\ (Data-Locations S)) by XBOOLE_1:16
.= (dom (NPP p)) /\ (dom (DataPart p)) by A3
.= dom (DataPart p) by A4, XBOOLE_1:28 ; :: thesis: verum