let s1, s2 be State of SCM+FSA ; :: thesis: ( s1,s2 equal_outside NAT implies for f being FinSeq-Location holds s1 . f = s2 . f )
assume A1: s1,s2 equal_outside NAT ; :: thesis: for f being FinSeq-Location holds s1 . f = s2 . f
let a be FinSeq-Location ; :: thesis: s1 . a = s2 . a
a in FinSeq-Locations by SCMFSA_2:10;
then A2: not a in NAT by SCMFSA_2:14, XBOOLE_0:3;
a in dom s2 by SCMFSA_2:67;
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:67;
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 ;
:: thesis: verum