let s1, s2 be State of SCM+FSA; ( s1,s2 equal_outside NAT implies for a being Int-Location holds s1 . a = s2 . a )
assume A1:
s1,s2 equal_outside NAT
; for a being Int-Location holds s1 . a = s2 . a
let a be Int-Location ; s1 . a = s2 . a
a in Int-Locations
by SCMFSA_2:9;
then A2:
not a in NAT
by SCMFSA_2:13, XBOOLE_0:3;
a in dom s2
by SCMFSA_2:66;
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 SCMFSA_2:66;
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, FUNCT_7:def 2
.=
s2 . a
by A3, FUNCT_1:71
;
verum