let s1, s2 be State of SCM+FSA; :: thesis: ( ( ( 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 )
A1: ((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT = (Data-Locations SCM+FSA) \/ ({(IC )} \/ NAT) by XBOOLE_1:4;

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: for x being set st x in Data-Locations SCM+FSA holds
s1 . x = s2 . x

hereby :: thesis: verum

let x be set ; :: thesis: ( x in Data-Locations SCM+FSA implies s1 . b₁ = s2 . b₁ )
assume A5: x in Data-Locations SCM+FSA ; :: thesis: s1 . b₁ = s2 . b₁

per cases ( x in Int-Locations or not x in Int-Locations ) ;

suppose x in Int-Locations ; :: thesis: s1 . b₁ = s2 . b₁

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

end;

suppose not x in Int-Locations ; :: thesis: s1 . b₁ = s2 . b₁

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

end;

end;

end;

end;

A6: now

assume A7: for x being set st x in Data-Locations SCM+FSA holds
s1 . x = s2 . x ; :: thesis: ( ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) )

hereby :: thesis: for f being FinSeq-Location holds s1 . f = s2 . f

let a be Int-Location ; :: thesis: s1 . a = s2 . a
a in Int-Locations by SCMFSA_2:9;
then a in Data-Locations SCM+FSA by XBOOLE_0:def 3, SCMFSA_2:127;
hence s1 . a = s2 . a by A7; :: thesis: verum

end;

hereby :: thesis: verum

let f be FinSeq-Location ; :: thesis: s1 . f = s2 . f
f in FinSeq-Locations by SCMFSA_2:10;
then f in Data-Locations SCM+FSA by XBOOLE_0:def 3, SCMFSA_2:127;
hence s1 . f = s2 . f by A7; :: thesis: verum

end;

end;

dom s2 = ((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT by COMPOS_1:172;
then A8: Data-Locations SCM+FSA c= dom s2 by A1, XBOOLE_1:7;
dom s1 = ((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT by COMPOS_1:172;
then Data-Locations SCM+FSA c= dom s1 by A1, 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:165; :: thesis: verum