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
A4: Int-Locations \/ FinSeq-Locations misses NAT by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;

now

assume IC SCM+FSA in NAT ; :: thesis: contradiction
then reconsider l = IC SCM+FSA as Instruction-Location of SCM+FSA by AMI_1:def 4;
l = IC SCM+FSA ;
hence contradiction by AMI_1:48; :: thesis: verum

end;

then {(IC SCM+FSA )} misses NAT by ZFMISC_1:56;
then A5: (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} misses NAT by A4, XBOOLE_1:70;
A6: 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 A5, XBOOLE_1:83 ;
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 A6, AMI_1:79 ;
A8: 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 A6, AMI_1:79 ;

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 A9: x in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} ; :: thesis: (s1 | ((dom s1) \ NAT )) . b₁ = (s2 | ((dom s2) \ NAT )) . b₁
then A10: ( 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 A10, XBOOLE_0:def 3;

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

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

end;

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

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

end;

suppose A13: 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, A9, FUNCT_1:70
.= IC s1 by A13, TARSKI:def 1
.= s2 . x by A1, A13, TARSKI:def 1
.= (s2 | ((dom s2) \ NAT )) . x by A8, A9, FUNCT_1:70 ; :: thesis: verum

end;

end;

end;

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