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

hereby :: thesis:

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

end;

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