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 COMPOS_1:3;
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