let s be State of SCM+FSA; :: according to EXTPRO_1:def 10,SCMFSA6B:def 3 :: thesis: ( not Initialize (Macro (halt SCM+FSA)) c= s or for b₁ being set holds
( not ProgramPart (Initialize (Macro (halt SCM+FSA))) c= b₁ or b₁ halts_on s ) )
set m = Macro (halt SCM+FSA);
set m1 = Initialize (Macro (halt SCM+FSA));
assume A1: Initialize (Macro (halt SCM+FSA)) c= s ; :: thesis: for b₁ being set holds
( not ProgramPart (Initialize (Macro (halt SCM+FSA))) c= b₁ or b₁ halts_on s )
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( not ProgramPart (Initialize (Macro (halt SCM+FSA))) c= P or P halts_on s )
assume A2: ProgramPart (Initialize (Macro (halt SCM+FSA))) c= P ; :: thesis: P halts_on s
A3: dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:19;
then A4: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def 1;
then A5: IC in dom (Initialize (Macro (halt SCM+FSA))) by FUNCT_4:13;
A6: IC (Initialize (Macro (halt SCM+FSA))) = (Start-At (0,SCM+FSA)) . (IC ) by A4, FUNCT_4:14
.= 0 by FUNCOP_1:87 ;
A7: 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
A8: 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 A8, XBOOLE_0:def 4;
then A9: x = IC by A3, TARSKI:def 1;
x in dom (Macro (halt SCM+FSA)) by A8, XBOOLE_0:def 4;
then ( x = 0 or x = 1 ) by A7, TARSKI:def 2;
hence contradiction by A9, 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 A10: ( (Macro (halt SCM+FSA)) . 0 = halt SCM+FSA & Macro (halt SCM+FSA) c= Initialize (Macro (halt SCM+FSA)) ) by FUNCT_4:33, FUNCT_4:66;
take 0 ; :: according to EXTPRO_1:def 7 :: thesis: ( IC (Comput (P,s,0)) in proj1 P & CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA )
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 0 in dom (Initialize (Macro (halt SCM+FSA))) by FUNCT_4:13;
then A12: 0 in dom (ProgramPart (Initialize (Macro (halt SCM+FSA)))) by COMPOS_1:16;
A13: Comput (P,s,0) = s by EXTPRO_1:3;
dom P = NAT by PARTFUN1:def 4;
hence IC (Comput (P,s,0)) in dom P ; :: thesis: CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA
dom P = NAT by PARTFUN1:def 4;
then CurInstr (P,(Comput (P,s,0))) = P . (IC s) by A13, PARTFUN1:def 8
.= P . (IC (Initialize (Macro (halt SCM+FSA)))) by A1, A5, GRFUNC_1:8
.= (ProgramPart (Initialize (Macro (halt SCM+FSA)))) . 0 by A6, GRFUNC_1:8, A2, A12
.= (Initialize (Macro (halt SCM+FSA))) . 0 by A12, FUNCT_1:70
.= halt SCM+FSA by A10, A11, GRFUNC_1:8 ;
hence CurInstr (P,(Comput (P,s,0))) = halt SCM+FSA ; :: thesis: verum