let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( Directed I is_pseudo-closed_on s & pseudo-LifeSpan s,(Directed I) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 )
let I be Program of SCM+FSA ; :: thesis: ( I is_closed_on s & I is_halting_on s implies ( Directed I is_pseudo-closed_on s & pseudo-LifeSpan s,(Directed I) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 ) )
set s1 = s +* (I +* (Start-At (insloc 0 )));
set s2 = s +* ((Directed I) +* (Start-At (insloc 0 )));
set m1 = LifeSpan (s +* (I +* (Start-At (insloc 0 ))));
assume A1: ( I is_closed_on s & I is_halting_on s ) ; :: thesis: ( Directed I is_pseudo-closed_on s & pseudo-LifeSpan s,(Directed I) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 )
ProgramPart (Directed I) = Directed I by AMI_1:105;
then A2: ( card I = card (ProgramPart (Directed I)) & dom I = dom (Directed I) ) by Th33, FUNCT_4:105;
then A3: IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card (ProgramPart (Directed I))) by A1, Th36;

A4: now

let n be Element of NAT ; :: thesis: ( n < (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 implies IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) in dom (Directed I) )
assume n < (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 ; :: thesis: IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) in dom (Directed I)
then n <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) by NAT_1:13;
then IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) by A1, Th35, AMI_1:121;
hence IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) in dom (Directed I) by A1, A2, SCMFSA7B:def 7; :: thesis: verum

end;

then A5: for n being Element of NAT st not IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) in dom (Directed I) holds
(LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 <= n ;
thus Directed I is_pseudo-closed_on s by A3, A4, Def3; :: thesis: pseudo-LifeSpan s,(Directed I) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1
hence pseudo-LifeSpan s,(Directed I) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 by A3, A5, Def5; :: thesis: verum