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

hereby :: thesis: ( IC s1 = IC s2 & DataPart s1 = DataPart s2 implies NPP s1 = NPP s2 )

assume A1: NPP s1 = NPP s2 ; :: thesis: ( IC s1 = IC s2 & DataPart s1 = DataPart s2 )
hence IC s1 = IC s2 by COMPOS_1:230; :: 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: NPP s1 = NPP s2
( ( 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 NPP s1 = NPP s2 by A2, SCMFSA10:91; :: thesis: verum