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 NPP s1 = NPP s2 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 NPP s1 = NPP s2 holds
IC s1 = IC s2
let s1, s2 be State of S; :: thesis: ( NPP s1 = NPP s2 implies IC s1 = IC s2 )
assume A1: NPP s1 = NPP s2 ; :: thesis: IC s1 = IC s2
A2: not IC in NAT by Def12;
X1: dom s1 = the carrier of S by PARTFUN1:def 4;
X2: dom s2 = the carrier of S by PARTFUN1:def 4;
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 = IC (s1 | ((dom s1) \ NAT)) by FUNCT_1:71
.= IC (NPP s1) by Th65, X1
.= IC (s2 | ((dom s2) \ NAT)) by A1, Th65, X2
.= IC s2 by A3, FUNCT_1:71 ;
:: thesis: verum