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)) . 0 = halt SCM+FSA & Macro (halt SCM+FSA) c= (Macro (halt SCM+FSA)) +* (Start-At (0,SCM+FSA)) ) by FUNCT_4:33, FUNCT_4:66;
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 )
dom (Macro (halt SCM+FSA)) = {0,1} by FUNCT_4:65;
then A10: 0 in dom (Macro (halt SCM+FSA)) by TARSKI:def 2;
then A11: 0 in dom ((Macro (halt SCM+FSA)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:13;
Z: (ProgramPart s) /. (IC s) = s . (IC s) by COMPOS_1:38;
Y: Comput ((ProgramPart s),s,0) = s by EXTPRO_1:3;
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
CurInstr ((ProgramPart (Comput ((ProgramPart s),s,0))),(Comput ((ProgramPart s),s,0))) = CurInstr ((ProgramPart s),s) by Y
.= s . (IC ((Macro (halt SCM+FSA)) +* (Start-At (0,SCM+FSA)))) by A1, A4, Z, GRFUNC_1:8
.= ((Macro (halt SCM+FSA)) +* (Start-At (0,SCM+FSA))) . 0 by A1, A11, A5, GRFUNC_1:8
.= halt SCM+FSA by A9, A10, GRFUNC_1:8 ;
hence CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,0))) = halt SCM+FSA by Y; :: thesis: verum