let s1, s2 be State of SCM+FSA ; :: thesis: for Iloc being Subset of Int-Locations holds
( s1 | (Iloc \/ FinSeq-Locations ) = s2 | (Iloc \/ FinSeq-Locations ) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location holds s1 . x = s2 . x ) ) )
let Iloc be Subset of Int-Locations ; :: thesis: ( s1 | (Iloc \/ FinSeq-Locations ) = s2 | (Iloc \/ FinSeq-Locations ) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location holds s1 . x = s2 . x ) ) )
set FSL = FinSeq-Locations ;
A1: [#] FinSeq-Locations = FinSeq-Locations ;
( ( ( for x being FinSeq-Location holds s1 . x = s2 . x ) implies for x being FinSeq-Location st x in FinSeq-Locations holds
s1 . x = s2 . x ) & ( ( for x being FinSeq-Location st x in FinSeq-Locations holds
s1 . x = s2 . x ) implies for x being FinSeq-Location holds s1 . x = s2 . x ) ) by SCMFSA_2:10;
hence ( s1 | (Iloc \/ FinSeq-Locations ) = s2 | (Iloc \/ FinSeq-Locations ) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location holds s1 . x = s2 . x ) ) ) by A1, Th6; :: thesis: verum