let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for s1, s2 being State of (Trivial-AMI IL,N) st IC s1 = IC s2 holds
s1 = s2
let N be with_non-empty_elements set ; :: thesis: for s1, s2 being State of (Trivial-AMI IL,N) st IC s1 = IC s2 holds
s1 = s2
set T = Trivial-AMI IL,N;
let s1, s2 be State of (Trivial-AMI IL,N); :: thesis: ( IC s1 = IC s2 implies s1 = s2 )
assume A1: IC s1 = IC s2 ; :: thesis: s1 = s2
A2: dom s1 = dom the Object-Kind of (Trivial-AMI IL,N) by CARD_3:18;
then A3: dom s1 = dom s2 by CARD_3:18;

now

let x be set ; :: thesis: ( x in dom s1 implies s1 . b₁ = s2 . b₁ )
A4: dom s1 = the carrier of (Trivial-AMI IL,N) by A2, FUNCT_2:def 1
.= succ IL by Def2 ;
assume A5: x in dom s1 ; :: thesis: s1 . b₁ = s2 . b₁
then A6: ( x in IL or x in {IL} ) by A4, XBOOLE_0:def 3;

per cases ( x in IL or x = IL ) by A6, TARSKI:def 1;

suppose A7: x in IL ; :: thesis: s1 . b₁ = s2 . b₁

then x <> IL ;
then not x in {IL} by TARSKI:def 1;
then A8: not x in dom (IL .--> IL) by FUNCOP_1:19;
A9: the Object-Kind of (Trivial-AMI IL,N) . x = ((IL --> {[0 ,{} ]}) +* (IL .--> IL)) . x by Def2
.= (IL --> {[0 ,{} ]}) . x by A8, FUNCT_4:12
.= {[0 ,{} ]} by A7, FUNCOP_1:13 ;
then A10: s2 . x in {[0 ,{} ]} by A2, A5, CARD_3:18;
s1 . x in {[0 ,{} ]} by A2, A5, A9, CARD_3:18;
hence s1 . x = [0 ,{} ] by TARSKI:def 1
.= s2 . x by A10, TARSKI:def 1 ;
:: thesis: verum

end;

suppose A11: x = IL ; :: thesis: s1 . b₁ = s2 . b₁

hence s1 . x = IC s1 by Def2
.= s2 . x by A1, A11, Def2 ;
:: thesis: verum

end;

end;

end;

hence s1 = s2 by A3, FUNCT_1:9; :: thesis: verum