let s1, s2 be State of SCMPDS ; :: thesis: ( IC s1 = IC s2 & ( for a being Int_position holds s1 . a = s2 . a ) & ( for i being Element of NAT holds s1 . i = s2 . i ) implies s1 = s2 )
assume that
A1: IC s1 = IC s2 and
A2: for a being Int_position holds s1 . a = s2 . a and
A3: for i being Element of NAT holds s1 . i = s2 . i ; :: thesis: s1 = s2
A5: dom s1 = the carrier of SCMPDS by PARTFUN1:def 4;
A7: dom s2 = the carrier of SCMPDS by PARTFUN1:def 4;

A8: now

let x be set ; :: thesis: ( x in SCM-Memory implies s1 . b₁ = s2 . b₁ )
assume x in SCM-Memory ; :: thesis: s1 . b₁ = s2 . b₁
then A9: ( x in {(IC SCMPDS )} \/ SCM-Data-Loc or x in NAT ) by Th6, XBOOLE_0:def 3;

per cases ( x in {(IC SCMPDS )} or x in SCM-Data-Loc or x in NAT ) by A9, XBOOLE_0:def 3;

suppose x in {(IC SCMPDS )} ; :: thesis: s1 . b₁ = s2 . b₁

then x = IC SCMPDS by TARSKI:def 1;
hence s1 . x = s2 . x by A1; :: thesis: verum

end;

suppose x in SCM-Data-Loc ; :: thesis: s1 . b₁ = s2 . b₁

then x is Int_position by Def2;
hence s1 . x = s2 . x by A2; :: thesis: verum

end;

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

then reconsider l = x as Element of NAT ;
s1 . l = s2 . l by A3;
hence s1 . x = s2 . x ; :: thesis: verum

end;

end;

end;

SCM-Memory = dom s1 by A5;
hence s1 = s2 by A7, A8, FUNCT_1:9; :: thesis: verum