let s1, s2 be State of SCMPDS; :: thesis: ( NPP s1 = NPP s2 iff ( IC s1 = IC s2 & DataPart s1 = DataPart s2 ) )
thus ( NPP s1 = NPP s2 implies ( IC s1 = IC s2 & DataPart s1 = DataPart s2 ) ) by COMPOS_1:138, COMPOS_1:230; :: thesis: ( IC s1 = IC s2 & DataPart s1 = DataPart s2 implies NPP s1 = NPP s2 )
assume that
A1: IC s1 = IC s2 and
A2: DataPart s1 = DataPart s2 ; :: thesis: NPP s1 = NPP s2
for a being Int_position holds s1 . a = s2 . a by A2, SCMPDS_4:23;
hence NPP s1 = NPP s2 by A1, SCMPDS_4:11; :: thesis: verum