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 +* (I ";" J)) = NAT by PARTFUN1:def 2;
A2: dom (P +* (Directed I)) = NAT by PARTFUN1:def 2;
set s2 = s +* (Initialize ((intloc 0) .--> 1));
A3: ( s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) & s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) ) by MEMSTR_0:44;
A4: (Directed I) ";" J = I ";" J ;
set s1 = s +* (Initialize ((intloc 0) .--> 1));
assume A5: I is_halting_on Initialized s,P ; :: thesis:
s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) by MEMSTR_0:44;
then A6: (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 = pseudo-LifeSpan ((Initialized s),P,(Directed I)) by A5, Lm2;
A7: Directed I is_pseudo-closed_on Initialized s,P by A5, Lm2;

hereby :: thesis:

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

end;

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