let s1, s2 be State of SCM+FSA; :: thesis: ( s1,s2 equal_outside NAT iff s1 | ((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) = s2 | ((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) )
set Y = NAT ;
set X = (Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)};
A1: ((((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) \/ NAT) \ NAT) \/ NAT = (((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) \/ NAT) \/ NAT by XBOOLE_1:39
.= ((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) \/ (NAT \/ NAT) by XBOOLE_1:4
.= NAT \/ ((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) ;
A2: NAT misses (((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) \/ NAT) \ NAT by XBOOLE_1:79;
A3: (Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)} misses NAT

proof

assume (Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)} meets NAT ; :: thesis: contradiction
then consider x being set such that
A4: x in (Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)} and
A5: x in NAT by XBOOLE_0:3;
A6: ( x in Int-Locations \/ FinSeq-Locations or x in {(IC SCM+FSA)} ) by A4, XBOOLE_0:def 3;

per cases ( x in Int-Locations or x in FinSeq-Locations or x = IC SCM+FSA ) by A6, TARSKI:def 1, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis: contradiction

hence contradiction by A5, SCMFSA_2:13, XBOOLE_0:3; :: thesis: verum

end;

suppose x in FinSeq-Locations ; :: thesis: contradiction

hence contradiction by A5, SCMFSA_2:14, XBOOLE_0:3; :: thesis: verum

end;

suppose A7: x = IC SCM+FSA ; :: thesis: contradiction

reconsider x = x as Element of NAT by A5;
x = IC SCM+FSA by A7;
hence contradiction by COMPOS_1:3; :: thesis: verum

end;

end;

end;

dom s2 = the carrier of SCM+FSA by PARTFUN1:def 4;
then A8: (dom s2) \ NAT = (Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)} by A1, A2, A3, SCMFSA_2:8, XBOOLE_1:72;
dom s1 = the carrier of SCM+FSA by PARTFUN1:def 4;
then (dom s1) \ NAT = (Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)} by A1, A2, A3, SCMFSA_2:8, XBOOLE_1:72;
hence ( s1,s2 equal_outside NAT iff s1 | ((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) = s2 | ((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) ) by A8, FUNCT_7:def 2; :: thesis: verum