let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S holds DataPart p = DataPart (NPP p)
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p being PartState of S holds DataPart p = DataPart (NPP p)
let p be PartState of S; :: thesis: DataPart p = DataPart (NPP p)
X: Data-Locations S = (the carrier of S \ {(IC S)}) \ NAT by XBOOLE_1:41;
(the carrier of S \ NAT ) /\ (Data-Locations S) = (the carrier of S /\ (Data-Locations S)) \ NAT by XBOOLE_1:49
.= (Data-Locations S) \ NAT by XBOOLE_1:28
.= (the carrier of S \ {(IC S)}) \ (NAT \/ NAT ) by X, XBOOLE_1:41
.= Data-Locations S by X ;
hence DataPart p = p | ((the carrier of S \ NAT ) /\ (Data-Locations S))
.= (p | (the carrier of S \ NAT )) | (Data-Locations S) by RELAT_1:100
.= (NPP p) | (Data-Locations S) by Th40
.= DataPart (NPP p) ;
:: thesis: verum