set D = Int-Locations \/ FinSeq-Locations ;
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 )
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 )
assume A3: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis: DataPart s1 = DataPart s2
A4: 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 ;

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 & x in Int-Locations \/ FinSeq-Locations ) by XBOOLE_0:def 4;

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

suppose A8: 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 A9: 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, A9
.= (DataPart s2) . x by A4, A5, FUNCT_1:70 ; :: thesis: verum

end;

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

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

end;

end;

end;

end;

suppose A11: 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 A3, A11
.= (DataPart s2) . x by A4, A5, FUNCT_1:70 ; :: thesis: verum

end;

suppose A12: 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, A12, SCMFSA6A:37, XBOOLE_0:def 4; :: thesis: verum

end;

suppose A13: x is Instruction-Location of SCM+FSA ; :: thesis: (DataPart s1) . b₁ = (DataPart s2) . b₁

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

end;

end;

end;

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