let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( Directed I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1 )
let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( Directed I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1 )
let I be Program of SCM+FSA; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies ( Directed I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1 ) )
set s1 = Initialize s;
set s2 = Initialize s;
set m1 = LifeSpan ((P +* I),(Initialize s));
assume that
A1: I is_closed_on s,P and
A2: I is_halting_on s,P ; :: thesis: ( Directed I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1 )
A3: dom I = dom (Directed I) by FUNCT_4:99;

A4: now :: thesis: for n being Element of NAT st n < (LifeSpan ((P +* I),(Initialize s))) + 1 holds
IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I)

let n be Element of NAT ; :: thesis: ( n < (LifeSpan ((P +* I),(Initialize s))) + 1 implies IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I) )
assume n < (LifeSpan ((P +* I),(Initialize s))) + 1 ; :: thesis: IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I)
then n <= LifeSpan ((P +* I),(Initialize s)) by NAT_1:13;
then Comput ((P +* I),(Initialize s),n) = Comput ((P +* (Directed I)),(Initialize s),n) by A1, A2, Th21;
then IC (Comput ((P +* I),(Initialize s),n)) = IC (Comput ((P +* (Directed I)),(Initialize s),n)) ;
hence IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I) by A1, A3, SCMFSA7B:def 6; :: thesis: verum

end;

card I = card (Directed I) by Th19;
then A5: IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card (Directed I) by A1, A2, Th22;
hence A6: Directed I is_pseudo-closed_on s,P by A4, Def2; :: thesis: pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1
for n being Element of NAT st not IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I) holds
(LifeSpan ((P +* I),(Initialize s))) + 1 <= n by A4;
hence pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1 by A5, A6, Def4; :: thesis: verum