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 s1, s2 being State of S st ProgramPart s1 = ProgramPart s2 & NPP s1 = NPP s2 holds
s1 = s2
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for s1, s2 being State of S st ProgramPart s1 = ProgramPart s2 & NPP s1 = NPP s2 holds
s1 = s2
let s1, s2 be State of S; :: thesis: ( ProgramPart s1 = ProgramPart s2 & NPP s1 = NPP s2 implies s1 = s2 )
assume Z: ( ProgramPart s1 = ProgramPart s2 & NPP s1 = NPP s2 ) ; :: thesis: s1 = s2
( s1 = (NPP s1) \/ (ProgramPart s1) & s2 = (NPP s2) \/ (ProgramPart s2) ) by Th68;
hence s1 = s2 by Z; :: thesis: verum