let s1, s2 be State of SCM+FSA; :: thesis: ( s1,s2 equal_outside NAT iff ( IC s1 = IC s2 & DataPart s1 = DataPart s2 ) )

hereby :: thesis: ( IC s1 = IC s2 & DataPart s1 = DataPart s2 implies s1,s2 equal_outside NAT )

assume A1: s1,s2 equal_outside NAT ; :: thesis: ( IC s1 = IC s2 & DataPart s1 = DataPart s2 )
hence IC s1 = IC s2 by COMPOS_1:24; :: thesis: DataPart s1 = DataPart s2
( ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) ) by A1, SCMFSA10:92, SCMFSA10:93;
hence DataPart s1 = DataPart s2 by SCMFSA6A:38; :: thesis: verum

end;

assume that
A2: IC s1 = IC s2 and
A3: DataPart s1 = DataPart s2 ; :: thesis: s1,s2 equal_outside NAT
( ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) ) by A3, SCMFSA6A:38;
hence s1,s2 equal_outside NAT by A2, SCMFSA10:91; :: thesis: verum