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 ) ) )
set FSL = FinSeq-Locations ;
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 ) ) )
A1: ( ( 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 ) ;
A2: ( ( 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:def 5;
[#] FinSeq-Locations = FinSeq-Locations ;
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, A2, Th27; :: thesis: verum