let s1, s2 be State of SCM+FSA; :: thesis: ( s1 . (intloc 0) = s2 . (intloc 0) & ( for a being read-write Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) implies DataPart s1 = DataPart s2 )
set D = Int-Locations \/ FinSeq-Locations;
assume A1: s1 . (intloc 0) = s2 . (intloc 0) ; :: thesis: ( ex a being read-write Int-Location st not s1 . a = s2 . a or ex f being FinSeq-Location st not s1 . f = s2 . f or DataPart s1 = DataPart s2 )
assume A2: for a being read-write Int-Location holds s1 . a = s2 . a ; :: thesis: ( ex f being FinSeq-Location st not s1 . f = s2 . f or DataPart s1 = DataPart s2 )
A3: dom (DataPart s1) = (dom s1) /\ (Int-Locations \/ FinSeq-Locations) by RELAT_1:90, SCMFSA_2:127
.= (((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) \/ NAT) /\ (Int-Locations \/ FinSeq-Locations) by SCMFSA6A:34
.= (dom s2) /\ (Int-Locations \/ FinSeq-Locations) by SCMFSA6A:34
.= dom (DataPart s2) by RELAT_1:90, SCMFSA_2:127 ;
assume A4: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis: DataPart s1 = DataPart s2

now

let x be set ; :: thesis: ( x in dom (DataPart s1) implies (DataPart s1) . b₁ = (DataPart s2) . b₁ )
assume A5: x in dom (DataPart s1) ; :: thesis: (DataPart s1) . b₁ = (DataPart s2) . b₁
then A6: x in (dom s1) /\ (Int-Locations \/ FinSeq-Locations) by RELAT_1:90, SCMFSA_2:127;
then A7: x in dom s1 by XBOOLE_0:def 4;
A8: x in Int-Locations \/ FinSeq-Locations by A6, XBOOLE_0:def 4;

per cases ( x is Int-Location or x is FinSeq-Location or x = IC SCM+FSA or x is Element of NAT ) by A7, SCMFSA6A:35;

suppose A9: x is Int-Location ; :: thesis: (DataPart s1) . b₁ = (DataPart s2) . b₁

hereby :: thesis: verum

per cases ( x is read-write Int-Location or not x is read-write Int-Location ) ;

suppose A10: x is read-write Int-Location ; :: thesis: (DataPart s1) . x = (DataPart s2) . x

thus (DataPart s1) . x = s1 . x by A5, FUNCT_1:70
.= s2 . x by A2, A10
.= (DataPart s2) . x by A3, A5, FUNCT_1:70 ; :: thesis: verum

end;

suppose A11: x is not read-write Int-Location ; :: thesis: (DataPart s1) . x = (DataPart s2) . x

reconsider a = x as Int-Location by A9;
a = intloc 0 by A11, SF_MASTR:def 5;
hence (DataPart s1) . x = s2 . a by A1, A5, FUNCT_1:70
.= (DataPart s2) . x by A3, A5, FUNCT_1:70 ;
:: thesis: verum

end;

end;

end;

end;

suppose A12: x is FinSeq-Location ; :: thesis: (DataPart s1) . b₁ = (DataPart s2) . b₁

thus (DataPart s1) . x = s1 . x by A5, FUNCT_1:70
.= s2 . x by A4, A12
.= (DataPart s2) . x by A3, A5, FUNCT_1:70 ; :: thesis: verum

end;

suppose A13: x = IC SCM+FSA ; :: thesis: (DataPart s1) . b₁ = (DataPart s2) . b₁

assume not (DataPart s1) . x = (DataPart s2) . x ; :: thesis: contradiction
thus contradiction by A6, A13, SCMFSA6A:37, XBOOLE_0:def 4; :: thesis: verum

end;

suppose A14: x is Element of NAT ; :: thesis: (DataPart s1) . b₁ = (DataPart s2) . b₁

assume not (DataPart s1) . x = (DataPart s2) . x ; :: thesis: contradiction
thus contradiction by A8, A14, SCMFSA6A:37; :: thesis: verum

end;

end;

end;

then DataPart s1 c= DataPart s2 by A3, GRFUNC_1:8;
hence DataPart s1 = DataPart s2 by A3, GRFUNC_1:9; :: thesis: verum