set m = Macro (halt SCM+FSA );
set m1 = (Macro (halt SCM+FSA )) +* (Start-At (insloc 0 ));
let s be State of SCM+FSA ; :: according to AMI_1:def 26,SCMFSA6B:def 3 :: thesis: ( not (Macro (halt SCM+FSA )) +* (Start-At (insloc 0 )) c= s or s is halting )
assume A1: (Macro (halt SCM+FSA )) +* (Start-At (insloc 0 )) c= s ; :: thesis: s is halting
A2: dom (Start-At (insloc 0 )) = {(IC SCM+FSA )} by FUNCOP_1:19;
then A3: IC SCM+FSA in dom (Start-At (insloc 0 )) by TARSKI:def 1;
then A4: IC SCM+FSA in dom ((Macro (halt SCM+FSA )) +* (Start-At (insloc 0 ))) by FUNCT_4:13;
A6: (Macro (halt SCM+FSA )) . (insloc 0 ) = halt SCM+FSA by FUNCT_4:66;
A7: dom (Macro (halt SCM+FSA )) = {(insloc 0 ),(insloc 1)} by FUNCT_4:65;

now

assume not (dom (Macro (halt SCM+FSA ))) /\ (dom (Start-At (insloc 0 ))) is empty ; :: thesis: contradiction
then consider x being set such that
A8: x in (dom (Macro (halt SCM+FSA ))) /\ (dom (Start-At (insloc 0 ))) by XBOOLE_0:def 1;
( x in dom (Macro (halt SCM+FSA )) & x in dom (Start-At (insloc 0 )) ) by A8, XBOOLE_0:def 4;
then ( ( x = insloc 0 or x = insloc 1 ) & x = IC SCM+FSA ) by A2, A7, TARSKI:def 1, TARSKI:def 2;
hence contradiction by AMI_1:48; :: thesis: verum

end;

then dom (Macro (halt SCM+FSA )) misses dom (Start-At (insloc 0 )) by XBOOLE_0:def 7;
then A9: Macro (halt SCM+FSA ) c= (Macro (halt SCM+FSA )) +* (Start-At (insloc 0 )) by FUNCT_4:33;
dom (Macro (halt SCM+FSA )) = {(insloc 0 ),(insloc 1)} by FUNCT_4:65;
then A10: insloc 0 in dom (Macro (halt SCM+FSA )) by TARSKI:def 2;
then A11: insloc 0 in dom ((Macro (halt SCM+FSA )) +* (Start-At (insloc 0 ))) by FUNCT_4:13;
A12: IC ((Macro (halt SCM+FSA )) +* (Start-At (insloc 0 ))) = ((Macro (halt SCM+FSA )) +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A4, AMI_1:def 43
.= (Start-At (insloc 0 )) . (IC SCM+FSA ) by A3, FUNCT_4:14
.= insloc 0 by FUNCOP_1:87 ;
take 0 ; :: according to AMI_1:def 20 :: thesis: CurInstr (Computation s,0 ) = halt SCM+FSA
thus CurInstr (Computation s,0 ) = CurInstr s by AMI_1:13
.= s . (IC ((Macro (halt SCM+FSA )) +* (Start-At (insloc 0 )))) by A1, A4, AMI_1:97
.= ((Macro (halt SCM+FSA )) +* (Start-At (insloc 0 ))) . (insloc 0 ) by A1, A11, A12, GRFUNC_1:8
.= halt SCM+FSA by A6, A9, A10, GRFUNC_1:8 ; :: thesis: verum