let s be State of ; :: thesis: for I being parahalting No-StopCode Program of st Initialized (stop I) c= s holds
IC (Computation s,(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I)
let I be parahalting No-StopCode Program of ; :: thesis: ( Initialized (stop I) c= s implies IC (Computation s,(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) )
set IsI = Initialized (stop I);
A1: stop I c= Initialized (stop I) by SCMPDS_4:9;
set Css = Computation s,(LifeSpan s);
reconsider n = IC (Computation s,(LifeSpan s)) as Element of NAT by ORDINAL1:def 13;
assume A2: Initialized (stop I) c= s ; :: thesis: IC (Computation s,(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I)
then A3: ProgramPart s halts_on s by SCMPDS_4:63;
I c= stop I by SCMPDS_4:40;
then I c= Initialized (stop I) by A1, XBOOLE_1:1;
then A4: I c= s by A2, XBOOLE_1:1;

now

assume A5: IC (Computation s,(LifeSpan s)) in dom I ; :: thesis: contradiction
then I . (IC (Computation s,(LifeSpan s))) = s . (IC (Computation s,(LifeSpan s))) by A4, GRFUNC_1:8
.= CurInstr (Computation s,(LifeSpan s)) by AMI_1:54
.= halt SCMPDS by A3, AMI_1:def 46 ;
hence contradiction by A5, Def3; :: thesis: verum

end;

then A6: n >= card I by SCMPDS_4:1;
A7: card (stop I) = (card I) + 1 by SCMPDS_4:45, SCMPDS_4:74;
IC (Computation s,(LifeSpan s)) in dom (stop I) by A2, SCMPDS_4:def 9;
then n < (card I) + 1 by A7, SCMPDS_4:1;
then n <= card I by NAT_1:13;
then n = card I by A6, XXREAL_0:1;
hence IC (Computation s,(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) by A2, FUNCT_4:79; :: thesis: verum