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 s1,s2 equal_outside NAT 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 s1,s2 equal_outside NAT holds
DataPart s1 = DataPart s2
let s1, s2 be State of S; :: thesis: ( s1,s2 equal_outside NAT implies DataPart s1 = DataPart s2 )
assume A1: s1,s2 equal_outside NAT ; :: thesis: DataPart s1 = DataPart s2
A2: dom (DataPart s1) = Data-Locations S by Th50
.= dom (DataPart s2) by Th50 ;
for x being set st x in dom (DataPart s1) holds
(DataPart s1) . x = (DataPart s2) . x

proof

let x be set ; :: thesis: ( x in dom (DataPart s1) implies (DataPart s1) . x = (DataPart s2) . x )
assume A3: x in dom (DataPart s1) ; :: thesis: (DataPart s1) . x = (DataPart s2) . x
dom (DataPart s1) c= dom s1 by RELAT_1:89;
then A4: x in dom s1 by A3;
dom (DataPart s1) misses NAT by Th137;
then not x in NAT by A3, XBOOLE_0:3;
then A5: x in (dom s1) \ NAT by A4, XBOOLE_0:def 5;
A6: dom s1 = the carrier of S by PARTFUN1:def 4
.= dom s2 by PARTFUN1:def 4 ;
thus (DataPart s1) . x = s1 . x by A3, FUNCT_1:70
.= (s1 | ((dom s1) \ NAT)) . x by A5, FUNCT_1:72
.= (s2 | ((dom s2) \ NAT)) . x by A1, FUNCT_7:def 2
.= s2 . x by A5, A6, FUNCT_1:72
.= (DataPart s2) . x by A3, A2, FUNCT_1:70 ; :: thesis: verum

end;

hence DataPart s1 = DataPart s2 by A2, FUNCT_1:def 17; :: thesis: verum