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 dom (NPP p) c= {(IC )} \/ (dom (DataPart 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 dom (NPP p) c= {(IC )} \/ (dom (DataPart p))
let p be PartState of S; :: thesis: dom (NPP p) c= {(IC )} \/ (dom (DataPart p))
set S0 = Start-At (0,S);

per cases ( IC in dom p or not IC in dom p ) ;

suppose IC in dom p ; :: thesis: dom (NPP p) c= {(IC )} \/ (dom (DataPart p))

hence dom (NPP p) c= {(IC )} \/ (dom (DataPart p)) by Th70; :: thesis: verum

end;

suppose A1: not IC in dom p ; :: thesis: dom (NPP p) c= {(IC )} \/ (dom (DataPart p))

A2: dom (Start-At (0,S)) = {(IC )} by FUNCOP_1:19;
IC in dom (p +* (Start-At (0,S))) by Th141;
then A3: dom (NPP (p +* (Start-At (0,S)))) = {(IC )} \/ (dom (DataPart (p +* (Start-At (0,S))))) by Th70
.= {(IC )} \/ (dom ((DataPart p) +* (DataPart (Start-At (0,S))))) by FUNCT_4:75
.= {(IC )} \/ (dom ((DataPart p) +* {})) by Th30
.= {(IC )} \/ (dom (DataPart p)) by FUNCT_4:22 ;

now

assume dom p meets dom (Start-At (0,S)) ; :: thesis: contradiction
then consider x being set such that
A4: x in dom p and
A5: x in dom (Start-At (0,S)) by XBOOLE_0:3;
x = IC by A2, A5, TARSKI:def 1;
hence contradiction by A4, A1; :: thesis: verum

end;

then p c= p +* (Start-At (0,S)) by FUNCT_4:33;
then NPP p c= NPP (p +* (Start-At (0,S))) by Th170;
then dom (NPP p) c= dom (NPP (p +* (Start-At (0,S)))) by RELAT_1:25;
hence dom (NPP p) c= {(IC )} \/ (dom (DataPart p)) by A3; :: thesis: verum

end;

end;