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

A5: now :: thesis: for x being set st x in SCM-Memory holds
s1 . x = s2 . x

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 A6: x in {(IC )} \/ SCM-Data-Loc by Th2;

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

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

then x = IC 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 AMI_2:def 16;
hence s1 . x = s2 . x by A2; :: thesis: verum

end;

end;

end;

SCM-Memory = dom s1 by A3;
hence s1 = s2 by A4, A5, FUNCT_1:2; :: thesis: verum