set D = Int-Locations \/ FinSeq-Locations ;
let s1, s2 be State of SCM+FSA ; :: thesis: ( IC s1 = IC s2 & DataPart s1 = DataPart s2 & s1 | NAT = s2 | NAT implies s1 = s2 )
assume A1: IC s1 = IC s2 ; :: thesis: ( not DataPart s1 = DataPart s2 or not s1 | NAT = s2 | NAT or s1 = s2 )
assume DataPart s1 = DataPart s2 ; :: thesis: ( not s1 | NAT = s2 | NAT or s1 = s2 )
then A2: ( ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) ) by SCMFSA6A:38;
assume s1 | NAT = s2 | NAT ; :: thesis: s1 = s2
then for l being Element of NAT holds s1 . l = s2 . l by SCMFSA6A:36;
hence s1 = s2 by A1, A2, SCMFSA_2:86; :: thesis: verum