let N be non empty with_non-empty_elements set ; :: thesis: for s1, s2 being State of (Trivial-COM N) st IC s1 = IC s2 holds
s1 = s2
set T = Trivial-COM N;
let s1, s2 be State of (Trivial-COM N); :: thesis: ( IC s1 = IC s2 implies s1 = s2 )
assume A1: IC s1 = IC s2 ; :: thesis: s1 = s2
A2: dom s1 = the carrier of (Trivial-COM N) by PARTFUN1:def 4;

A3: now

let x be set ; :: thesis: ( x in dom s1 implies s1 . b₁ = s2 . b₁ )
assume A4: x in dom s1 ; :: thesis: s1 . b₁ = s2 . b₁
dom s1 = the carrier of (Trivial-COM N) by PARTFUN1:def 4
.= succ NAT by Def2 ;
then A5: ( x in NAT or x in {NAT} ) by A4, XBOOLE_0:def 3;

per cases ( x in NAT or x = NAT ) by A5, TARSKI:def 1;

suppose A6: x in NAT ; :: thesis: s1 . b₁ = s2 . b₁

then x <> NAT ;
then not x in {NAT} by TARSKI:def 1;
then A7: not x in dom (NAT .--> NAT) by FUNCOP_1:19;
A8: the Object-Kind of (Trivial-COM N) . x = ((NAT --> {[0,{},{}]}) +* (NAT .--> NAT)) . x by Def2
.= (NAT --> {[0,{},{}]}) . x by A7, FUNCT_4:12
.= {[0,{},{}]} by A6, FUNCOP_1:13 ;
x in dom s2 by A2, A4, PARTFUN1:def 4;
then A9: s2 . x in {[0,{},{}]} by A8, FUNCT_1:def 20;
s1 . x in {[0,{},{}]} by A4, A8, FUNCT_1:def 20;
hence s1 . x = [0,{},{}] by TARSKI:def 1
.= s2 . x by A9, TARSKI:def 1 ;
:: thesis: verum

end;

suppose A10: x = NAT ; :: thesis: s1 . b₁ = s2 . b₁

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

end;

end;

end;

dom s1 = dom s2 by A2, PARTFUN1:def 4;
hence s1 = s2 by A3, FUNCT_1:9; :: thesis: verum