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 Z1: s1,s2 equal_outside NAT ; :: thesis: DataPart s1 = DataPart s2
A: 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 Z: x in dom (DataPart s1) ; :: thesis: (DataPart s1) . x = (DataPart s2) . x
dom (DataPart s1) c= dom s1 by RELAT_1:89;
then C: x in dom s1 by Z;
dom (DataPart s1) misses NAT by Th137;
then not x in NAT by Z, XBOOLE_0:3;
then B1: x in (dom s1) \ NAT by C, XBOOLE_0:def 5;
B2: dom s1 = the carrier of S by PARTFUN1:def 4
.= dom s2 by PARTFUN1:def 4 ;
thus (DataPart s1) . x = s1 . x by Z, FUNCT_1:70
.= (s1 | ((dom s1) \ NAT)) . x by B1, FUNCT_1:72
.= (s2 | ((dom s2) \ NAT)) . x by Z1, FUNCT_7:def 2
.= s2 . x by B1, B2, FUNCT_1:72
.= (DataPart s2) . x by Z, A, FUNCT_1:70 ; :: thesis: verum

end;

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