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 = Initialize s;
A5: (Directed I) ';' J = I ';' J by Th41;
set s1 = Initialize s;
assume A6: I is_halting_on s,P ; :: thesis:
then A7: (LifeSpan ((P +* I),(Initialize s))) + 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),(Initialize s)) ; :: thesis:
then A9: k < pseudo-LifeSpan (s,P,(Directed I)) by A7, NAT_1:13;
then A10: IC (Comput ((P +* (Directed I)),(Initialize s),k)) in dom (Directed I) by A8, Def5, A1;
NPP (Comput ((P +* (Directed I)),(Initialize s),k)) = NPP (Comput ((P +* (I ';' J)),(Initialize s),k)) by A5, A8, A9, Th32;
hence A11: IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ';' J)),(Initialize s),k)) by COMPOS_1:230; :: thesis:
A13: Directed I c= I ';' J by SCMFSA6A:55;
then B14: dom (Directed I) c= dom (I ';' J) by GRFUNC_1:8;
thus CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A2, PARTFUN1:def 8
.= (Directed I) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A10, FUNCT_4:14
.= (I ';' J) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A10, A13, GRFUNC_1:8
.= (P +* (I ';' J)) . (IC (Comput ((P +* (I ';' J)),(Initialize s),k))) by A11, B14, FUNCT_4:14, A10
.= CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(Initialize s),k))) by A3, PARTFUN1:def 8 ; :: thesis:

end;

NPP (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = NPP (Comput ((P +* (I ';' J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) by A4, A6, A5, A7, Lm2, Th32;
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))) ) by COMPOS_1:230, COMPOS_1:138; :: thesis: