let R be non trivial good Ring; :: thesis: for s1, s2 being State of (SCM R) st IC s1 = IC s2 & ( for a being Data-Location of R holds s1 . a = s2 . a ) holds
NPP s1 = NPP s2
let s1, s2 be State of (SCM R); :: thesis: ( IC s1 = IC s2 & ( for a being Data-Location of R holds s1 . a = s2 . a ) implies NPP s1 = NPP s2 )
assume A1: IC s1 = IC s2 ; :: thesis: ( ex a being Data-Location of R st not s1 . a = s2 . a or NPP s1 = NPP s2 )
( IC in dom s1 & IC in dom s2 ) by COMPOS_1:9;
then X1: ( NPP s1 = (DataPart s1) +* (Start-At ((IC s1),(SCM R))) & NPP s2 = (DataPart s2) +* (Start-At ((IC s2),(SCM R))) ) by COMPOS_1:74;
assume B2: for a being Data-Location of R holds s1 . a = s2 . a ; :: thesis: NPP s1 = NPP s2
DataPart s1 = DataPart s2

proof

B1: dom (DataPart s1) = Data-Locations (SCM R) by COMPOS_1:50;
hence dom (DataPart s1) = dom (DataPart s2) by COMPOS_1:50; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in proj1 (DataPart s1) or (DataPart s1) . b₁ = (DataPart s2) . b₁ )
let x be set ; :: thesis: ( not x in proj1 (DataPart s1) or (DataPart s1) . x = (DataPart s2) . x )
assume Z: x in dom (DataPart s1) ; :: thesis: (DataPart s1) . x = (DataPart s2) . x
then A2: x is Data-Location of R by B1, SCMRING2:32;
thus (DataPart s1) . x = s1 . x by Z, B1, FUNCT_1:72
.= s2 . x by A2, B2
.= (DataPart s2) . x by Z, B1, FUNCT_1:72 ; :: thesis: verum

end;

hence NPP s1 = NPP s2 by A1, X1; :: thesis: verum