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

A1: now :: thesis:

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

hereby :: thesis:

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

per cases ;

suppose x in Int-Locations ; :: thesis:

then x is Int-Location by AMI_2:def 16;
hence s1 . x = s2 . x by A2; :: thesis:

end;

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

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

end;

end;

end;

end;

A5: now :: thesis:

assume A6: 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 AMI_2:def 16;
then a in Data-Locations by SCMFSA_2:100, XBOOLE_0:def 3;
hence s1 . a = s2 . a by A6; :: thesis:

end;

hereby :: thesis:

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

end;

end;

dom s2 = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13;
then A7: 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 A7, A1, A5, FUNCT_1:95; :: thesis: