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 holds dom (NPP s) = {(IC S)} \/ (dom (DataPart s))
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for s being State of S holds dom (NPP s) = {(IC S)} \/ (dom (DataPart s))
let s be State of S; :: thesis: dom (NPP s) = {(IC S)} \/ (dom (DataPart s))
IC S in dom s by Th9;
hence dom (NPP s) = {(IC S)} \/ (dom (DataPart s)) by Th45; :: thesis: verum