let s be 0 -started State of SCMPDS; :: thesis: for I being parahalting Program of SCMPDS
for k being Element of NAT st k < LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I))) holds
IC (Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k)) in dom I
let I be parahalting Program of SCMPDS; :: thesis: for k being Element of NAT st k < LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I))) holds
IC (Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k)) in dom I
let k be Element of NAT ; :: thesis: ( k < LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I))) implies IC (Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k)) in dom I )
set ss = s +* (stop I);
set m = LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I)));
set Sk = Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k);
set Ik = IC (Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k));
A1: ProgramPart (s +* (stop I)) halts_on s +* (stop I) by FUNCT_4:26, SCMPDS_4:def 10;
reconsider n = IC (Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k)) as Element of NAT ;
A3: IC (Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k)) in dom (stop I) by FUNCT_4:26, SCMPDS_4:def 9;
A4: stop I c= s +* (stop I) by FUNCT_4:26;
assume A5: k < LifeSpan ((ProgramPart (s +* (stop I))),(s +* (stop I))) ; :: thesis: IC (Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k)) in dom I

A6: now

assume A7: n = card I ; :: thesis: contradiction
y: 0 in dom (Stop SCMPDS) by COMPOS_1:45;
x: (Stop SCMPDS) . 0 = halt SCMPDS by AFINSQ_1:38;
CurInstr ((ProgramPart (s +* (stop I))),(Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k))) = (s +* (stop I)) . (IC (Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k))) by COMPOS_1:38
.= (stop I) . (0 + n) by A3, A4, GRFUNC_1:8
.= halt SCMPDS by A7, x, y, AFINSQ_1:def 4 ;
hence contradiction by A5, A1, EXTPRO_1:def 14; :: thesis: verum

end;

card (stop I) = (card I) + 1 by LL, AFINSQ_1:20;
then n < (card I) + 1 by A3, AFINSQ_1:70;
then n <= card I by INT_1:20;
then n < card I by A6, XXREAL_0:1;
hence IC (Comput ((ProgramPart (s +* (stop I))),(s +* (stop I)),k)) in dom I by AFINSQ_1:70; :: thesis: verum