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
A4: dom s1 = the carrier of SCMPDS by PARTFUN1:def 2;
A5: dom s2 = the carrier of SCMPDS by PARTFUN1:def 2;

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

per cases ( x in {(IC )} or x in SCM-Data-Loc ) by A7, 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 Def2;
hence s1 . x = s2 . x by A2; :: thesis: verum

end;

end;

end;

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