let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite COM-Struct of N
for s1, s2 being State of S holds ProgramPart (s1 +* (DataPart s2)) = ProgramPart s1
let S be non empty stored-program IC-Ins-separated definite COM-Struct of N; :: thesis: for s1, s2 being State of S holds ProgramPart (s1 +* (DataPart s2)) = ProgramPart s1
let s1, s2 be State of S; :: thesis: ProgramPart (s1 +* (DataPart s2)) = ProgramPart s1
NAT c= {(IC S)} \/ NAT by XBOOLE_1:7;
then Data-Locations S misses NAT by XBOOLE_1:85;
then X: ProgramPart (DataPart s2) = {} by RELAT_1:207;
thus ProgramPart (s1 +* (DataPart s2)) = (ProgramPart s1) +* (ProgramPart (DataPart s2)) by FUNCT_4:75
.= ProgramPart s1 by X, FUNCT_4:22 ; :: thesis: verum