let s1, s2 be State of SCM+FSA; :: thesis:
let Iloc be Subset of Int-Locations; :: thesis:
let Floc be Subset of FinSeq-Locations; :: thesis:
FinSeq-Locations c= dom s1 by SCMFSA_2:46;
then A1: Floc c= dom s1 ;
FinSeq-Locations c= dom s2 by SCMFSA_2:46;
then A2: Floc c= dom s2 ;
Int-Locations c= dom s2 by SCMFSA_2:45;
then A3: Iloc c= dom s2 ;
then A4: Iloc \/ Floc c= dom s2 by A2, XBOOLE_1:8;
Int-Locations c= dom s1 by SCMFSA_2:45;
then A5: Iloc c= dom s1 ;
then A6: Iloc \/ Floc c= dom s1 by A1, XBOOLE_1:8;

hereby :: thesis:

assume A7: s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc) ; :: thesis:

hereby :: thesis:

let x be Int-Location; :: thesis:
assume x in Iloc ; :: thesis:
then x in Iloc \/ Floc by XBOOLE_0:def 3;
hence s1 . x = s2 . x by A6, A4, A7, FUNCT_1:95; :: thesis:

end;

let x be FinSeq-Location ; :: thesis:
assume x in Floc ; :: thesis:
then x in Iloc \/ Floc by XBOOLE_0:def 3;
hence s1 . x = s2 . x by A6, A4, A7, FUNCT_1:95; :: thesis:

end;

assume that
A8: for x being Int-Location st x in Iloc holds
s1 . x = s2 . x and
A9: for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x ; :: thesis:

A10: now :: thesis:

hereby :: thesis:

let x be set ; :: thesis:
assume A11: x in Iloc ; :: thesis:
then x in Int-Locations ;
then reconsider x9 = x as Int-Location by AMI_2:def 16;
thus s1 . x = s2 . x9 by A8, A11
.= s2 . x ; :: thesis:

end;

let x be set ; :: thesis:
assume A12: x in Floc ; :: thesis:
then x in FinSeq-Locations ;
then reconsider x9 = x as FinSeq-Location by SCMFSA_2:def 5;
thus s1 . x = s2 . x9 by A9, A12
.= s2 . x ; :: thesis:

end;

then A13: s1 | Floc = s2 | Floc by A1, A2, FUNCT_1:95;
s1 | Iloc = s2 | Iloc by A5, A3, A10, FUNCT_1:95;
hence s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc) by A13, RELAT_1:150; :: thesis: