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 s being State of S
for p being PartState of S holds (NPP s) | (dom (DataPart p)) = s | (dom (DataPart p))
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for s being State of S
for p being PartState of S holds (NPP s) | (dom (DataPart p)) = s | (dom (DataPart p))
let s be State of S; :: thesis: for p being PartState of S holds (NPP s) | (dom (DataPart p)) = s | (dom (DataPart p))
let p be PartState of S; :: thesis: (NPP s) | (dom (DataPart p)) = s | (dom (DataPart p))
dom (DataPart p) c= Data-Locations S by RELAT_1:87;
then A: dom (DataPart p) c= (Data-Locations S) \/ {(IC )} by XBOOLE_1:10;
thus (NPP s) | (dom (DataPart p)) = (s | ((Data-Locations S) \/ {(IC )})) | (dom (DataPart p)) by LmAA
.= s | (dom (DataPart p)) by A, RELAT_1:103 ; :: thesis: verum