let s be State of SCM+FSA; :: thesis: for I being InitHalting Program of SCM+FSA st Initialized I c= s holds
for k being Element of NAT st k <= LifeSpan ((ProgramPart s),s) holds
CurInstr ((ProgramPart (s +* (loop I))),(Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))) <> halt SCM+FSA
let I be InitHalting Program of SCM+FSA; :: thesis: ( Initialized I c= s implies for k being Element of NAT st k <= LifeSpan ((ProgramPart s),s) holds
CurInstr ((ProgramPart (s +* (loop I))),(Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))) <> halt SCM+FSA )
set s2 = s +* (loop I);
assume A1: Initialized I c= s ; :: thesis: for k being Element of NAT st k <= LifeSpan ((ProgramPart s),s) holds
CurInstr ((ProgramPart (s +* (loop I))),(Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))) <> halt SCM+FSA
then A2: ProgramPart s halts_on s by EXTPRO_1:def 10;

hereby :: thesis: verum

let k be Element of NAT ; :: thesis: ( k <= LifeSpan ((ProgramPart s),s) implies not CurInstr ((ProgramPart (s +* (loop I))),(Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))) = halt SCM+FSA )
set lk = IC (Comput ((ProgramPart s),s,k));
A3: ( IC (Comput ((ProgramPart s),s,k)) in dom I & dom I = dom (loop I) ) by A1, Def1, FUNCT_4:105;
then A4: (loop I) . (IC (Comput ((ProgramPart s),s,k))) in rng (loop I) by FUNCT_1:def 5;
T2: ProgramPart (s +* (loop I)) = ProgramPart (Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k)) by AMI_1:123;
Y: (ProgramPart (s +* (loop I))) /. (IC (Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))) = (Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k)) . (IC (Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))) by T2, COMPOS_1:38;
assume k <= LifeSpan ((ProgramPart s),s) ; :: thesis: not CurInstr ((ProgramPart (s +* (loop I))),(Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))) = halt SCM+FSA
then IC (Comput ((ProgramPart s),s,k)) = IC (Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k)) by A1, A2, Th65, COMPOS_1:24;
then A5: CurInstr ((ProgramPart (s +* (loop I))),(Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))) = (s +* (loop I)) . (IC (Comput ((ProgramPart s),s,k))) by Y, AMI_1:54
.= (loop I) . (IC (Comput ((ProgramPart s),s,k))) by A3, FUNCT_4:14 ;
assume CurInstr ((ProgramPart (s +* (loop I))),(Comput ((ProgramPart (s +* (loop I))),(s +* (loop I)),k))) = halt SCM+FSA ; :: thesis: contradiction
hence contradiction by A5, A4, SCMFSA8C:107; :: thesis: verum

end;