let s be State of SCMPDS; :: thesis: for I being Program of SCMPDS
for i being Element of NAT st Initialize (stop I) c= s & I is_closed_on s & I is_halting_on s & i < LifeSpan ((ProgramPart s),s) holds
IC (Comput ((ProgramPart s),s,i)) in dom I
let I be Program of SCMPDS; :: thesis: for i being Element of NAT st Initialize (stop I) c= s & I is_closed_on s & I is_halting_on s & i < LifeSpan ((ProgramPart s),s) holds
IC (Comput ((ProgramPart s),s,i)) in dom I
let i be Element of NAT ; :: thesis: ( Initialize (stop I) c= s & I is_closed_on s & I is_halting_on s & i < LifeSpan ((ProgramPart s),s) implies IC (Comput ((ProgramPart s),s,i)) in dom I )
set sI = stop I;
set Ci = Comput ((ProgramPart s),s,i);
set Lc = IC (Comput ((ProgramPart s),s,i));
assume that
A1: Initialize (stop I) c= s and
A2: I is_closed_on s and
A3: I is_halting_on s and
A4: i < LifeSpan ((ProgramPart s),s) ; :: thesis: IC (Comput ((ProgramPart s),s,i)) in dom I
I1: s +* (Initialize (stop I)) = (Initialize s) +* (stop I) by COMPOS_1:125;
A5: s = (Initialize s) +* (stop I) by A1, I1, FUNCT_4:79;
then A6: IC (Comput ((ProgramPart s),s,i)) in dom (stop I) by A2, SCMPDS_6:def 2;
stop I c= Initialize (stop I) by COMPOS_1:126;
then A7: stop I c= s by A1, XBOOLE_1:1;
A8: ProgramPart s halts_on s by A3, A5, SCMPDS_6:def 3;

now

assume A9: (stop I) . (IC (Comput ((ProgramPart s),s,i))) = halt SCMPDS ; :: thesis: contradiction
TX: ProgramPart (Comput ((ProgramPart s),s,i)) = ProgramPart s by AMI_1:123;
Y: (ProgramPart (Comput ((ProgramPart s),s,i))) /. (IC (Comput ((ProgramPart s),s,i))) = (Comput ((ProgramPart s),s,i)) . (IC (Comput ((ProgramPart s),s,i))) by COMPOS_1:38;
CurInstr ((ProgramPart (Comput ((ProgramPart s),s,i))),(Comput ((ProgramPart s),s,i))) = s . (IC (Comput ((ProgramPart s),s,i))) by Y, AMI_1:54
.= halt SCMPDS by A6, A7, A9, GRFUNC_1:8 ;
hence contradiction by A4, A8, TX, EXTPRO_1:def 14; :: thesis: verum

end;

hence IC (Comput ((ProgramPart s),s,i)) in dom I by A6, SCMPDS_5:3; :: thesis: verum