set A = NAT ;
let s1, s2 be State of SCM+FSA ; :: thesis: ( IC s1 = IC s2 & ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) implies s1,s2 equal_outside NAT )
assume that
A1: IC s1 = IC s2 and
A2: for a being Int-Location holds s1 . a = s2 . a and
A3: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis: s1,s2 equal_outside NAT
not IC SCM+FSA in NAT by AMI_1:48;
then ( Int-Locations \/ FinSeq-Locations misses NAT & {(IC SCM+FSA )} misses NAT ) by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70, ZFMISC_1:56;
then A4: (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} misses NAT by XBOOLE_1:70;
A5: the carrier of SCM+FSA \ NAT = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \ NAT by SCMFSA_2:8, XBOOLE_1:40
.= (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A4, XBOOLE_1:83 ;
A6: dom (s2 | ((dom s2) \ NAT )) = (dom s2) /\ ((dom s2) \ NAT ) by RELAT_1:90
.= (dom s2) \ NAT by XBOOLE_1:28
.= (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A5, PARTFUN1:def 4 ;
A7: dom (s1 | ((dom s1) \ NAT )) = (dom s1) /\ ((dom s1) \ NAT ) by RELAT_1:90
.= (dom s1) \ NAT by XBOOLE_1:28
.= (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A5, PARTFUN1:def 4 ;

now

let x be set ; :: thesis: ( x in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} implies (s1 | ((dom s1) \ NAT )) . b₁ = (s2 | ((dom s2) \ NAT )) . b₁ )
assume A8: x in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} ; :: thesis: (s1 | ((dom s1) \ NAT )) . b₁ = (s2 | ((dom s2) \ NAT )) . b₁
then A9: ( x in Int-Locations \/ FinSeq-Locations or x in {(IC SCM+FSA )} ) by XBOOLE_0:def 3;

per cases ( x in Int-Locations or x in FinSeq-Locations or x in {(IC SCM+FSA )} ) by A9, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: (s1 | ((dom s1) \ NAT )) . b₁ = (s2 | ((dom s2) \ NAT )) . b₁

then A10: x is Int-Location by SCMFSA_2:11;
thus (s1 | ((dom s1) \ NAT )) . x = s1 . x by A7, A8, FUNCT_1:70
.= s2 . x by A2, A10
.= (s2 | ((dom s2) \ NAT )) . x by A6, A8, FUNCT_1:70 ; :: thesis: verum

end;

suppose x in FinSeq-Locations ; :: thesis: (s1 | ((dom s1) \ NAT )) . b₁ = (s2 | ((dom s2) \ NAT )) . b₁

then A11: x is FinSeq-Location by SCMFSA_2:12;
thus (s1 | ((dom s1) \ NAT )) . x = s1 . x by A7, A8, FUNCT_1:70
.= s2 . x by A3, A11
.= (s2 | ((dom s2) \ NAT )) . x by A6, A8, FUNCT_1:70 ; :: thesis: verum

end;

suppose A12: x in {(IC SCM+FSA )} ; :: thesis: (s1 | ((dom s1) \ NAT )) . b₁ = (s2 | ((dom s2) \ NAT )) . b₁

thus (s1 | ((dom s1) \ NAT )) . x = s1 . x by A7, A8, FUNCT_1:70
.= IC s1 by A12, TARSKI:def 1
.= s2 . x by A1, A12, TARSKI:def 1
.= (s2 | ((dom s2) \ NAT )) . x by A6, A8, FUNCT_1:70 ; :: thesis: verum

end;

end;

end;

hence s1 | ((dom s1) \ NAT ) = s2 | ((dom s2) \ NAT ) by A7, A6, FUNCT_1:9; :: according to FUNCT_7:def 2 :: thesis: verum