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: ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT = (Int-Locations \/ FinSeq-Locations ) \/ ({(IC SCM+FSA )} \/ NAT ) by XBOOLE_1:4;
dom s1 = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by AMI_1:79, SCMFSA_2:8;
then A2: Int-Locations \/ FinSeq-Locations c= dom s1 by A1, XBOOLE_1:7;
dom s2 = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by AMI_1:79, SCMFSA_2:8;
then A3: Int-Locations \/ FinSeq-Locations c= dom s2 by A1, XBOOLE_1:7;

A4: now

assume A5: ( ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) ) ; :: thesis: for x being set st x in Int-Locations \/ FinSeq-Locations holds
s1 . x = s2 . x

hereby :: thesis: verum

let x be set ; :: thesis: ( x in Int-Locations \/ FinSeq-Locations implies s1 . b₁ = s2 . b₁ )
assume A6: x in Int-Locations \/ FinSeq-Locations ; :: 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 A5; :: thesis: verum

end;

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

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

end;

end;

end;

end;

now

assume A7: for x being set st x in Int-Locations \/ FinSeq-Locations 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 Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
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 Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 3;
hence s1 . f = s2 . f by A7; :: thesis: verum

end;

end;

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 A2, A3, A4, FUNCT_1:165, SCMFSA_2:127; :: thesis: verum