let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated realistic COM-Struct of N
for s1, s2 being State of S st s1,s2 equal_outside NAT holds
IC s1 = IC s2
let S be non empty IC-Ins-separated realistic COM-Struct of N; :: thesis: for s1, s2 being State of S st s1,s2 equal_outside NAT holds
IC s1 = IC s2
let s1, s2 be State of S; :: thesis: ( s1,s2 equal_outside NAT implies IC s1 = IC s2 )
assume A1: s1,s2 equal_outside NAT ; :: thesis: IC s1 = IC s2
A2: not IC in NAT by Def12;
IC in dom s2 by Lm6;
then IC in (dom s2) \ NAT by A2, XBOOLE_0:def 5;
then A3: IC in (dom s2) /\ ((dom s2) \ NAT) by XBOOLE_0:def 4;
IC in dom s1 by Lm6;
then IC in (dom s1) \ NAT by A2, XBOOLE_0:def 5;
then IC in (dom s1) /\ ((dom s1) \ NAT) by XBOOLE_0:def 4;
hence IC s1 = (s1 | ((dom s1) \ NAT)) . (IC ) by FUNCT_1:71
.= (s2 | ((dom s2) \ NAT)) . (IC ) by A1, FUNCT_7:def 2
.= IC s2 by A3, FUNCT_1:71 ;
:: thesis: verum