let s1, s2 be State of SCMPDS; :: thesis: ( NPP s1 = NPP s2 iff s1 | (SCM-Data-Loc \/ {(IC )}) = s2 | (SCM-Data-Loc \/ {(IC )}) )
set Y = NAT ;
set X = SCM-Data-Loc \/ {(IC )};
X1: ( NPP s1 = s1 | ((Data-Locations SCMPDS) \/ {(IC )}) & NPP s2 = s2 | ((Data-Locations SCMPDS) \/ {(IC )}) ) by COMPOS_1:231;
X2: Data-Locations SCMPDS = SCM-Data-Loc by SCMPDS_2:100;
thus ( NPP s1 = NPP s2 iff s1 | (SCM-Data-Loc \/ {(IC )}) = s2 | (SCM-Data-Loc \/ {(IC )}) ) by X1, X2; :: thesis: verum