let s1, s2 be State of SCMPDS; :: thesis: ( NPP s1 = NPP s2 implies for a being Int_position holds s1 . a = s2 . a )
assume A1: NPP s1 = NPP s2 ; :: thesis: for a being Int_position holds s1 . a = s2 . a
X1: ( s1 | ((dom s1) \ NAT) = NPP s1 & s2 | ((dom s2) \ NAT) = NPP s2 ) by COMPOS_1:232;
let a be Int_position ; :: thesis: s1 . a = s2 . a
a in SCM-Data-Loc by SCMPDS_2:def 2;
then A2: not a in NAT by AMI_2:29, XBOOLE_0:3;
a in dom s2 by SCMPDS_2:49;
then a in (dom s2) \ NAT by A2, XBOOLE_0:def 5;
then A3: a in (dom s2) /\ ((dom s2) \ NAT) by XBOOLE_0:def 4;
a in dom s1 by SCMPDS_2:49;
then a in (dom s1) \ NAT by A2, XBOOLE_0:def 5;
then a in (dom s1) /\ ((dom s1) \ NAT) by XBOOLE_0:def 4;
hence s1 . a = (s1 | ((dom s1) \ NAT)) . a by FUNCT_1:71
.= (s2 | ((dom s2) \ NAT)) . a by A1, X1
.= s2 . a by A3, FUNCT_1:71 ;
:: thesis: verum