let s1, s2 be State of SCM+FSA; :: thesis:

A2: now

assume that
A3: for a being Int-Location holds s1 . a = s2 . a and
A4: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis:

hereby :: thesis:

let x be set ; :: thesis:
assume A5: x in Data-Locations ; :: thesis:

per cases ;

suppose x in Int-Locations ; :: thesis:

then x is Int-Location by SCMFSA_2:4;
hence s1 . x = s2 . x by A3; :: thesis:

end;

suppose not x in Int-Locations ; :: thesis:

then x in FinSeq-Locations by A5, SCMFSA_2:100, XBOOLE_0:def 3;
then x is FinSeq-Location by SCMFSA_2:5;
hence s1 . x = s2 . x by A4; :: thesis:

end;

end;

end;

end;

A6: now

assume A7: for x being set st x in Data-Locations holds
s1 . x = s2 . x ; :: thesis:

hereby :: thesis:

let a be Int-Location ; :: thesis:
a in Int-Locations by SCMFSA_2:2;
then a in Data-Locations by SCMFSA_2:100, XBOOLE_0:def 3;
hence s1 . a = s2 . a by A7; :: thesis:

end;

hereby :: thesis:

let f be FinSeq-Location ; :: thesis:
f in FinSeq-Locations by SCMFSA_2:3;
then f in Data-Locations by SCMFSA_2:100, XBOOLE_0:def 3;
hence s1 . f = s2 . f by A7; :: thesis:

end;

end;

dom s2 = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13;
then A8: Data-Locations c= dom s2 by XBOOLE_1:7;
dom s1 = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13;
then Data-Locations c= dom s1 by XBOOLE_1:7;
hence ( ( ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) ) iff DataPart s1 = DataPart s2 ) by A8, A2, A6, FUNCT_1:95; :: thesis: