let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program realistic COM-Struct of N
for s1, s2 being State of S holds
( s1,s2 equal_outside NAT iff s1 | ((Data-Locations S) \/ {(IC )}) = s2 | ((Data-Locations S) \/ {(IC )}) )
let S be non empty stored-program realistic COM-Struct of N; :: thesis: for s1, s2 being State of S holds
( s1,s2 equal_outside NAT iff s1 | ((Data-Locations S) \/ {(IC )}) = s2 | ((Data-Locations S) \/ {(IC )}) )
let s1, s2 be State of S; :: thesis: ( s1,s2 equal_outside NAT iff s1 | ((Data-Locations S) \/ {(IC )}) = s2 | ((Data-Locations S) \/ {(IC )}) )
thus ( s1,s2 equal_outside NAT implies s1 | ((Data-Locations S) \/ {(IC )}) = s2 | ((Data-Locations S) \/ {(IC )}) ) :: thesis: ( s1 | ((Data-Locations S) \/ {(IC )}) = s2 | ((Data-Locations S) \/ {(IC )}) implies s1,s2 equal_outside NAT )

proof

assume A1: s1,s2 equal_outside NAT ; :: thesis: s1 | ((Data-Locations S) \/ {(IC )}) = s2 | ((Data-Locations S) \/ {(IC )})
A2: Data-Locations S misses NAT by Th51;
not IC in NAT by Def12;
then {(IC )} misses NAT by ZFMISC_1:56;
then (Data-Locations S) \/ {(IC )} misses NAT by A2, XBOOLE_1:70;
hence s1 | ((Data-Locations S) \/ {(IC )}) = s2 | ((Data-Locations S) \/ {(IC )}) by A1, FUNCT_7:139; :: thesis: verum

end;

assume A3: s1 | ((Data-Locations S) \/ {(IC )}) = s2 | ((Data-Locations S) \/ {(IC )}) ; :: thesis: s1,s2 equal_outside NAT
the carrier of S = ((Data-Locations S) \/ {(IC )}) \/ NAT by Th160;
hence s1,s2 equal_outside NAT by A3, FUNCT_7:138; :: thesis: verum