let s1, s2 be State of SCM+FSA ; :: thesis:
set X = (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )};
set Y = NAT ;
A1: dom s1 = the carrier of SCM+FSA by AMI_1:79;
A2: dom s2 = the carrier of SCM+FSA by AMI_1:79;
A3: ((((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 )}) ;
A4: NAT misses (((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT ) \ NAT by XBOOLE_1:79;
A5: (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} misses NAT

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

per cases by A7, TARSKI:def 1, XBOOLE_0:def 3;

suppose x in Int-Locations ; :: thesis:

hence contradiction by A6, SCMFSA_2:13, XBOOLE_0:3; :: thesis:

end;

suppose x in FinSeq-Locations ; :: thesis:

hence contradiction by A6, SCMFSA_2:14, XBOOLE_0:3; :: thesis:

end;

suppose A8: x = IC SCM+FSA ; :: thesis:

reconsider x = x as Instruction-Location of SCM+FSA by A6, AMI_1:def 4;
x = IC SCM+FSA by A8;
hence contradiction by AMI_1:48; :: thesis:

end;

end;

end;

then A9: (dom s1) \ NAT = (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A1, A3, A4, SCMFSA_2:8, XBOOLE_1:72;
(dom s2) \ NAT = (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} by A2, A3, A4, A5, 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 A9, FUNCT_7:def 2; :: thesis: