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 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 in dom p holds
IC (NPP p) = IC p
let p be PartState of S; :: thesis: ( IC in dom p implies IC (NPP p) = IC p )
dom p c= the carrier of S by RELAT_1:def 18;
then A1: NPP p = p | ( the carrier of S \ NAT) by RELAT_1:211;
assume IC in dom p ; :: thesis: IC (NPP p) = IC p
then A2: dom (NPP p) = {(IC )} \/ (dom (DataPart p)) by Th70;
IC in {(IC )} by TARSKI:def 1;
then IC in dom (NPP p) by A2, XBOOLE_0:def 3;
hence IC (NPP p) = IC p by A1, FUNCT_1:70; :: thesis: verum