let s1, s2 be State of SCM+FSA; :: thesis: ( IC s1 = IC s2 & ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) implies s1 = s2 )
assume A1: IC s1 = IC s2 ; :: thesis: ( ex a being Int-Location st not s1 . a = s2 . a or ex f being FinSeq-Location st not s1 . f = s2 . f or s1 = s2 )
( IC in dom s1 & IC in dom s2 ) by MEMSTR_0:2;
then X1: ( s1 = (DataPart s1) +* (Start-At ((IC s1),SCM+FSA)) & s2 = (DataPart s2) +* (Start-At ((IC s2),SCM+FSA)) ) by MEMSTR_0:26;
assume that
B2: for a being Int-Location holds s1 . a = s2 . a and
C2: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis: s1 = s2
DataPart s1 = DataPart s2

proof

B1: dom (DataPart s1) = Data-Locations by MEMSTR_0:9;
hence dom (DataPart s1) = dom (DataPart s2) by MEMSTR_0:9; :: according to FUNCT_1:def 11 :: thesis: for b₁ being set holds
( not b₁ in proj1 (DataPart s1) or (DataPart s1) . b₁ = (DataPart s2) . b₁ )
let x be set ; :: thesis: ( not x in proj1 (DataPart s1) or (DataPart s1) . x = (DataPart s2) . x )
assume Z: x in dom (DataPart s1) ; :: thesis: (DataPart s1) . x = (DataPart s2) . x
then pc: x in Int-Locations \/ FinSeq-Locations by B1, Th127;

per cases ( x in Int-Locations or x in FinSeq-Locations ) by pc, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: (DataPart s1) . x = (DataPart s2) . x

then A2: x is Int-Location by Th11;
thus (DataPart s1) . x = s1 . x by Z, B1, FUNCT_1:49
.= s2 . x by A2, B2
.= (DataPart s2) . x by Z, B1, FUNCT_1:49 ; :: thesis: verum

end;

suppose x in FinSeq-Locations ; :: thesis: (DataPart s1) . x = (DataPart s2) . x

then A2: x is FinSeq-Location by Th12;
thus (DataPart s1) . x = s1 . x by Z, B1, FUNCT_1:49
.= s2 . x by A2, C2
.= (DataPart s2) . x by Z, B1, FUNCT_1:49 ; :: thesis: verum

end;

end;

end;

hence s1 = s2 by A1, X1; :: thesis: verum