let s be State of ; :: according to AMI_1:def 26,SCMFSA6B:def 3 :: thesis: ( not (Macro (halt SCM+FSA )) +* (Start-At (insloc 0 )) c= s or ProgramPart s halts_on s )
set m = Macro (halt SCM+FSA );
set m1 = (Macro (halt SCM+FSA )) +* (Start-At (insloc 0 ));
assume A1: (Macro (halt SCM+FSA )) +* (Start-At (insloc 0 )) c= s ; :: thesis: ProgramPart s halts_on s
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;
then A5: IC ((Macro (halt SCM+FSA )) +* (Start-At (insloc 0 ))) = ((Macro (halt SCM+FSA )) +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by AMI_1:def 43
.= (Start-At (insloc 0 )) . (IC SCM+FSA ) by A3, FUNCT_4:14
.= insloc 0 by FUNCOP_1:87 ;
A6: 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
A7: x in (dom (Macro (halt SCM+FSA ))) /\ (dom (Start-At (insloc 0 ))) by XBOOLE_0:def 1;
x in dom (Start-At (insloc 0 )) by A7, XBOOLE_0:def 4;
then A8: x = IC SCM+FSA by A2, TARSKI:def 1;
x in dom (Macro (halt SCM+FSA )) by A7, XBOOLE_0:def 4;
then ( x = insloc 0 or x = insloc 1 ) by A6, TARSKI:def 2;
hence contradiction by A8, 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;
take 0 ; :: according to AMI_1:def 20 :: thesis: ( IC (Computation s,0 ) in dom (ProgramPart s) & (ProgramPart s) . (IC (Computation s,0 )) = halt SCM+FSA )
IC (Computation s,0 ) in NAT by AMI_1:def 4;
hence IC (Computation s,0 ) in dom (ProgramPart s) by AMI_1:143; :: thesis: (ProgramPart s) . (IC (Computation s,0 )) = halt SCM+FSA
A10: (Macro (halt SCM+FSA )) . (insloc 0 ) = halt SCM+FSA by FUNCT_4:66;
dom (Macro (halt SCM+FSA )) = {(insloc 0 ),(insloc 1)} by FUNCT_4:65;
then A11: insloc 0 in dom (Macro (halt SCM+FSA )) by TARSKI:def 2;
then A12: insloc 0 in dom ((Macro (halt SCM+FSA )) +* (Start-At (insloc 0 ))) by FUNCT_4:13;
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, A12, A5, GRFUNC_1:8
.= halt SCM+FSA by A10, A9, A11, GRFUNC_1:8 ;
hence (ProgramPart s) . (IC (Computation s,0 )) = halt SCM+FSA by AMI_1:145; :: thesis: verum