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