let s be State of SCM+FSA; :: according to EXTPRO_1:def 10,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 EXTPRO_1:def 7 :: 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 EXTPRO_1:3;
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