let s be State of SCM+FSA; :: thesis:
let P be Instruction-Sequence of SCM+FSA; :: thesis:
let I be really-closed Program of SCM+FSA; :: thesis:
let J be Program of SCM+FSA; :: thesis:
A1: dom (P +* (Directed I)) = NAT by PARTFUN1:def 2;
A2: dom (P +* (I ";" J)) = NAT by PARTFUN1:def 2;
set s2 = Initialize s;
A3: (Directed I) ";" J = I ";" J ;
set s1 = Initialize s;
assume A4: I is_halting_on s,P ; :: thesis:
then A5: (LifeSpan ((P +* I),(Initialize s))) + 1 = pseudo-LifeSpan (s,P,(Directed I)) by Lm2;
A6: Directed I is_pseudo-closed_on s,P by A4, Lm2;

hereby :: thesis:

let k be Nat; :: thesis:
assume k <= LifeSpan ((P +* I),(Initialize s)) ; :: thesis:
then A7: k < pseudo-LifeSpan (s,P,(Directed I)) by A5, NAT_1:13;
then A8: IC (Comput ((P +* (Directed I)),(Initialize s),k)) in dom (Directed I) by A6, Def3;
Comput ((P +* (Directed I)),(Initialize s),k) = Comput ((P +* (I ";" J)),(Initialize s),k) by A3, A4, Lm2, A7, Th11;
hence A9: IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) ; :: thesis:
A10: Directed I c= I ";" J by SCMFSA6A:16;
then A11: dom (Directed I) c= dom (I ";" J) by GRFUNC_1:2;
thus CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A1, PARTFUN1:def 6
.= (Directed I) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A8, FUNCT_4:13
.= (I ";" J) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A8, A10, GRFUNC_1:2
.= (P +* (I ";" J)) . (IC (Comput ((P +* (I ";" J)),(Initialize s),k))) by A9, A11, A8, FUNCT_4:13
.= CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) by A2, PARTFUN1:def 6 ; :: thesis:

end;

Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)) = Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)) by A4, A3, A5, Lm2, Th11;
hence ( DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) ) ; :: thesis: