let s1, s2 be State of SCM+FSA ; :: thesis: ( s1,s2 equal_outside NAT implies DataPart s1 = DataPart s2 )
assume s1,s2 equal_outside NAT ; :: thesis: DataPart s1 = DataPart s2
then ( ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) ) by SCMFSA10:92, SCMFSA10:93;
hence DataPart s1 = DataPart s2 by Th38; :: thesis: verum