let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being Program of
for i being Nat st stop I c= P & I is_closed_on s,P & I is_halting_on s,P & i < LifeSpan (P,s) holds
IC (Comput (P,s,i)) in dom I

let s be 0 -started State of SCMPDS; :: thesis: for I being Program of
for i being Nat st stop I c= P & I is_closed_on s,P & I is_halting_on s,P & i < LifeSpan (P,s) holds
IC (Comput (P,s,i)) in dom I

let I be Program of ; :: thesis: for i being Nat st stop I c= P & I is_closed_on s,P & I is_halting_on s,P & i < LifeSpan (P,s) holds
IC (Comput (P,s,i)) in dom I

let i be Nat; :: thesis: ( stop I c= P & I is_closed_on s,P & I is_halting_on s,P & i < LifeSpan (P,s) implies IC (Comput (P,s,i)) in dom I )
set sI = stop I;
set Ci = Comput (P,s,i);
set Lc = IC (Comput (P,s,i));
assume that
A1: stop I c= P and
A2: I is_closed_on s,P and
A3: I is_halting_on s,P and
A4: i < LifeSpan (P,s) ; :: thesis: IC (Comput (P,s,i)) in dom I
A5: Start-At (0,SCMPDS) c= s by MEMSTR_0:29;
A6: P +* (stop I) = P by ;
A7: s = Initialize s by ;
then A8: IC (Comput (P,s,i)) in dom (stop I) by ;
A9: P halts_on s by ;
now :: thesis: not (stop I) . (IC (Comput (P,s,i))) = halt SCMPDS
assume A10: (stop I) . (IC (Comput (P,s,i))) = halt SCMPDS ; :: thesis: contradiction
CurInstr (P,(Comput (P,s,i))) = P . (IC (Comput (P,s,i))) by PBOOLE:143
.= halt SCMPDS by ;
hence contradiction by A4, A9, EXTPRO_1:def 15; :: thesis: verum
end;
hence IC (Comput (P,s,i)) in dom I by ; :: thesis: verum