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

now

assume not (dom (Macro (halt SCM+FSA ))) /\ (dom (Start-At 0 ,SCM+FSA )) is empty ; :: thesis: contradiction
then consider x being set such that
A7: x in (dom (Macro (halt SCM+FSA ))) /\ (dom (Start-At 0 ,SCM+FSA )) by XBOOLE_0:def 1;
x in dom (Start-At 0 ,SCM+FSA ) 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 = 0 or x = 1 ) by A6, TARSKI:def 2;
hence contradiction by A8, COMPOS_1:3; :: thesis: verum

end;

then dom (Macro (halt SCM+FSA )) misses dom (Start-At 0 ,SCM+FSA ) by XBOOLE_0:def 7;
then A9: Macro (halt SCM+FSA ) c= (Macro (halt SCM+FSA )) +* (Start-At 0 ,SCM+FSA ) by FUNCT_4:33;
take 0 ; :: according to AMI_1:def 20 :: thesis: ( IC (Comput (ProgramPart s),s,0 ) in proj1 (ProgramPart s) & CurInstr (ProgramPart s),(Comput (ProgramPart s),s,0 ) = halt SCM+FSA )
IC (Comput (ProgramPart s),s,0 ) in NAT ;
hence IC (Comput (ProgramPart s),s,0 ) in dom (ProgramPart s) by COMPOS_1:34; :: thesis: CurInstr (ProgramPart s),(Comput (ProgramPart s),s,0 ) = halt SCM+FSA
A10: (Macro (halt SCM+FSA )) . 0 = halt SCM+FSA by FUNCT_4:66;
dom (Macro (halt SCM+FSA )) = {0 ,1} by FUNCT_4:65;
then A11: 0 in dom (Macro (halt SCM+FSA )) by TARSKI:def 2;
then A12: 0 in dom ((Macro (halt SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:13;
Y: (ProgramPart s) /. (IC s) = s . (IC s) by COMPOS_1:38;
Comput (ProgramPart s),s,0 = s by AMI_1:13;
then CurInstr (ProgramPart s),(Comput (ProgramPart s),s,0 ) = CurInstr (ProgramPart s),s
.= s . (IC ((Macro (halt SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) by A1, A4, Y, GRFUNC_1:8
.= ((Macro (halt SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) . 0 by A1, A12, A5, GRFUNC_1:8
.= halt SCM+FSA by A10, A9, A11, GRFUNC_1:8 ;
hence CurInstr (ProgramPart s),(Comput (ProgramPart s),s,0 ) = halt SCM+FSA ; :: thesis: verum