let l be Instruction-Location of SCM+FSA ; :: thesis: not l in dom (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))
assume l in dom (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) ; :: thesis: contradiction
then ( l = intloc 0 or l = IC SCM+FSA ) by Th1;
hence contradiction by AMI_1:48, SCMFSA_2:84; :: thesis: verum