let s be State of ; :: thesis: for l being Instruction-Location of SCM+FSA holds dom (s | NAT ) misses dom (Start-At l)
let l be Instruction-Location of SCM+FSA ; :: thesis: dom (s | NAT ) misses dom (Start-At l)

now

let x be set ; :: thesis: ( x in dom (s | NAT ) implies not x in dom (Start-At l) )
assume x in dom (s | NAT ) ; :: thesis: not x in dom (Start-At l)
then x in NAT by Th3;
then x is Instruction-Location of SCM+FSA by AMI_1:def 4;
then x <> IC SCM+FSA by AMI_1:48;
then not x in {(IC SCM+FSA )} by TARSKI:def 1;
hence not x in dom (Start-At l) by FUNCOP_1:19; :: thesis: verum

end;

hence dom (s | NAT ) misses dom (Start-At l) by XBOOLE_0:3; :: thesis: verum