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: the carrier of SCMPDS = {(IC )} \/ SCM-Data-Loc by SCMPDS_2:84, STRUCT_0:4
.= {(IC )} \/ SCM-Data-Loc ;
A4: dom (s2 | (dom s2)) = (dom s2) /\ (dom s2) by RELAT_1:61
.= dom s2
.= {(IC )} \/ SCM-Data-Loc by A3, PARTFUN1:def 2 ;
A5: dom (s1 | (dom s1)) = (dom s1) /\ (dom s1) by RELAT_1:61
.= dom s1
.= {(IC )} \/ SCM-Data-Loc by A3, PARTFUN1:def 2 ;
A6: ( s1 | (dom s1) = s1 & s2 | (dom s2) = s2 ) by RELAT_1:69;

now :: thesis: for x being object st x in {(IC )} \/ SCM-Data-Loc holds
(s1 | (dom s1)) . x = (s2 | (dom s2)) . x

let x be object ; :: thesis: ( x in {(IC )} \/ SCM-Data-Loc implies (s1 | (dom s1)) . b₁ = (s2 | (dom s2)) . b₁ )
assume A7: x in {(IC )} \/ SCM-Data-Loc ; :: thesis: (s1 | (dom s1)) . b₁ = (s2 | (dom s2)) . b₁

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

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

then A8: x = IC by TARSKI:def 1;
hence (s1 | (dom s1)) . x = IC s1 by A5, A7, FUNCT_1:47
.= (s2 | (dom s2)) . x by A1, A4, A7, A8, FUNCT_1:47 ;
:: thesis: verum

end;

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

then A9: x is Int_position by AMI_2:def 16;
thus (s1 | (dom s1)) . x = s1 . x by A5, A7, FUNCT_1:47
.= s2 . x by A2, A9
.= (s2 | (dom s2)) . x by A4, A7, FUNCT_1:47 ; :: thesis: verum

end;

end;

end;

hence s1 = s2 by A6, A5, A4, FUNCT_1:2; :: thesis: verum