let R be good Ring; :: thesis: for a being Data-Location of R
for s1, s2 being State of (SCM R) st s1,s2 equal_outside NAT holds
s1 . a = s2 . a
let a be Data-Location of R; :: thesis: for s1, s2 being State of (SCM R) st s1,s2 equal_outside NAT holds
s1 . a = s2 . a
let s1, s2 be State of (SCM R); :: thesis: ( s1,s2 equal_outside NAT implies s1 . a = s2 . a )
set IL = NAT ;
assume A1: s1,s2 equal_outside NAT ; :: thesis: s1 . a = s2 . a
A2: dom s1 = the carrier of (SCM R) by AMI_1:79;
A3: dom s2 = the carrier of (SCM R) by AMI_1:79;
A4: not a in NAT by Th2;
then a in (dom s1) \ NAT by A2, XBOOLE_0:def 5;
then A5: a in (dom s1) /\ ((dom s1) \ NAT ) by XBOOLE_0:def 4;
a in (dom s2) \ NAT by A3, A4, XBOOLE_0:def 5;
then A6: a in (dom s2) /\ ((dom s2) \ NAT ) by XBOOLE_0:def 4;
thus s1 . a = (s1 | ((dom s1) \ NAT )) . a by A5, FUNCT_1:71
.= (s2 | ((dom s2) \ NAT )) . a by A1, FUNCT_7:def 2
.= s2 . a by A6, FUNCT_1:71 ; :: thesis: verum