let s be State of ; :: thesis:
let I, J be Program of ; :: thesis:
assume A1: I is_closed_on s ; :: thesis:
set s2 = s +* ((I ';' J) +* (Start-At (insloc 0 )));
A2: (Directed I) ';' J = I ';' J by Th41;
set s1 = s +* (I +* (Start-At (insloc 0 )));
assume A3: I is_halting_on s ; :: thesis:
then A4: (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 = pseudo-LifeSpan s,(Directed I) by A1, Lm2;
A5: Directed I is_pseudo-closed_on s by A1, A3, Lm2;

hereby :: thesis:

A6: I ';' J c= (I ';' J) +* (Start-At (insloc 0 )) by Th9;
then A7: dom (I ';' J) c= dom ((I ';' J) +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
let k be Element of NAT ; :: thesis:
A8: Directed I c= (Directed I) +* (Start-At (insloc 0 )) by Th9;
then A9: dom (Directed I) c= dom ((Directed I) +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
assume k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) ; :: thesis:
then A10: k < pseudo-LifeSpan s,(Directed I) by A4, NAT_1:13;
then A11: IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k) in dom (Directed I) by A5, Def5;
thus A12: IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k) = IC (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),k) by A2, A5, A10, Th32, AMI_1:121; :: thesis:
A13: Directed I c= I ';' J by SCMFSA6A:55;
then A14: dom (Directed I) c= dom (I ';' J) by GRFUNC_1:8;
then A15: IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k) in dom (I ';' J) by A11;
thus CurInstr (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k) = (s +* ((Directed I) +* (Start-At (insloc 0 )))) . (IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k)) by AMI_1:54
.= ((Directed I) +* (Start-At (insloc 0 ))) . (IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k)) by A11, A9, FUNCT_4:14
.= (Directed I) . (IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k)) by A11, A8, GRFUNC_1:8
.= (I ';' J) . (IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k)) by A11, A13, GRFUNC_1:8
.= ((I ';' J) +* (Start-At (insloc 0 ))) . (IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k)) by A11, A14, A6, GRFUNC_1:8
.= (s +* ((I ';' J) +* (Start-At (insloc 0 )))) . (IC (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),k)) by A12, A15, A7, FUNCT_4:14
.= CurInstr (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),k) by AMI_1:54 ; :: thesis:

end;

Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1), Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) equal_outside NAT by A1, A3, A2, A4, Lm2, Th32;
hence ( DataPart (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = DataPart (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) & IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = IC (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) ) by AMI_1:121, SCMFSA6A:39; :: thesis: