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 NPP s1 = NPP s2 holds
DataPart s1 = DataPart 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 NPP s1 = NPP s2 holds
DataPart s1 = DataPart s2
let s1, s2 be State of S; :: thesis: ( NPP s1 = NPP s2 implies DataPart s1 = DataPart s2 )
assume NPP s1 = NPP s2 ; :: thesis: DataPart s1 = DataPart s2
hence DataPart s1 = DataPart (NPP s2) by Th73
.= DataPart s2 by Th73 ;
:: thesis: verum