let s1, s2 be State of SCM+FSA; :: thesis:
set D = Data-Locations ;
assume A1: s1 . (intloc 0) = s2 . (intloc 0) ; :: thesis:
assume A2: for a being read-write Int-Location holds s1 . a = s2 . a ; :: thesis:
A3: dom (DataPart s1) = (dom s1) /\ (Data-Locations ) by RELAT_1:61
.= ((Data-Locations ) \/ {(IC )}) /\ (Data-Locations ) by MEMSTR_0:13
.= (dom s2) /\ (Data-Locations ) by MEMSTR_0:13
.= dom (DataPart s2) by RELAT_1:61 ;
assume A4: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis:

let x be object ; :: thesis:
assume A5: x in dom (DataPart s1) ; :: thesis:
then A6: x in (dom s1) /\ (Data-Locations ) by RELAT_1:61;
then A7: x in dom s1 by XBOOLE_0:def 4;

per cases by A7, Th1;

suppose A8: x is Int-Location ; :: thesis:

hereby :: thesis:

suppose A9: x is read-write Int-Location ; :: thesis:

thus (DataPart s1) . x = s1 . x by A5, FUNCT_1:47
.= s2 . x by A2, A9
.= (DataPart s2) . x by A3, A5, FUNCT_1:47 ; :: thesis:

end;

suppose A10: x is not read-write Int-Location ; :: thesis:

reconsider a = x as Int-Location by A8;
a = intloc 0 by A10, Def2;
hence (DataPart s1) . x = s2 . a by A1, A5, FUNCT_1:47
.= (DataPart s2) . x by A3, A5, FUNCT_1:47 ;
:: thesis:

end;

end;

end;

end;

suppose A11: x is FinSeq-Location ; :: thesis:

thus (DataPart s1) . x = s1 . x by A5, FUNCT_1:47
.= s2 . x by A4, A11
.= (DataPart s2) . x by A3, A5, FUNCT_1:47 ; :: thesis:

end;

suppose x = IC ; :: thesis:

then not x in Data-Locations by STRUCT_0:3;
hence (DataPart s1) . x = (DataPart s2) . x by A6, XBOOLE_0:def 4; :: thesis:

end;

end;

end;

then DataPart s1 c= DataPart s2 by A3, GRFUNC_1:2;
hence DataPart s1 = DataPart s2 by A3, GRFUNC_1:3; :: thesis: