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 st IC S in dom p holds
IC (NPP p) = IC p
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p being PartState of S st IC S in dom p holds
IC (NPP p) = IC p
let p be PartState of S; :: thesis: ( IC S in dom p implies IC (NPP p) = IC p )
dom p c= the carrier of S by RELAT_1:def 18;
then F: NPP p = p | ( the carrier of S \ NAT) by RELAT_1:211;
assume IC S in dom p ; :: thesis: IC (NPP p) = IC p
then X: dom (NPP p) = {(IC S)} \/ (dom (DataPart p)) by Th45;
IC S in {(IC S)} by TARSKI:def 1;
then IC S in dom (NPP p) by X, XBOOLE_0:def 3;
hence IC (NPP p) = IC p by F, FUNCT_1:70; :: thesis: verum