let s be State of SCM+FSA; :: thesis:
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis:
let I, J be Program of SCM+FSA; :: thesis:
A1: ProgramPart (Directed I) = Directed I by RELAT_1:209;
A2: dom (P +* (Directed I)) = NAT by PARTFUN1:def 4;
A3: dom (P +* (I ';' J)) = NAT by PARTFUN1:def 4;
assume A4: I is_closed_on s,P ; :: thesis:
set s2 = s +* (Initialize (I ';' J));
A5: (Directed I) ';' J = I ';' J by Th41;
set s1 = s +* (Initialize I);
assume A6: I is_halting_on s,P ; :: thesis:
then A7: (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 = pseudo-LifeSpan (s,P,(Directed I)) by A4, Lm2;
A8: Directed I is_pseudo-closed_on s,P by A4, A6, Lm2;

hereby :: thesis:

let k be Element of NAT ; :: thesis:
assume k <= LifeSpan ((P +* I),(s +* (Initialize I))) ; :: thesis:
then A9: k < pseudo-LifeSpan (s,P,(Directed I)) by A7, NAT_1:13;
then A10: IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k)) in dom (Directed I) by A8, Def5, A1;
thus A11: IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k)) = IC (Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),k)) by A5, A8, A9, Th32, COMPOS_1:24; :: thesis:
A12: (P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k))) by A2, PARTFUN1:def 8;
A13: Directed I c= I ';' J by SCMFSA6A:55;
then dom (Directed I) c= dom (I ';' J) by GRFUNC_1:8;
then A14: IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k)) in dom (I ';' J) by A10;
thus CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k))) by A12
.= (Directed I) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k))) by A10, FUNCT_4:14
.= (Directed I) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k)))
.= (I ';' J) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k))) by A10, A13, GRFUNC_1:8
.= (I ';' J) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k)))
.= (P +* (I ';' J)) . (IC (Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),k))) by A11, A14, FUNCT_4:14
.= CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),k))) by A3, PARTFUN1:def 8 ; :: thesis:

end;

Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1)), Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1)) equal_outside NAT by A4, A6, A5, A7, Lm2, Th32;
hence ( DataPart (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) = DataPart (Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) & IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) = IC (Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) ) by COMPOS_1:24, COMPOS_1:138; :: thesis: