let s1, s2 be State of SCM+FSA; :: thesis:
set D = Int-Locations \/ FinSeq-Locations;
let I be Program of SCM+FSA; :: thesis:
assume A1: I is_closed_on s1 ; :: thesis:
set ss2 = s2 +* (I +* (Start-At (0,SCM+FSA)));
set ss1 = s1 +* (I +* (Start-At (0,SCM+FSA)));
assume A2: I is_halting_on s1 ; :: thesis:
assume A3: DataPart s1 = DataPart s2 ; :: thesis:
A4: I c= I +* (Start-At (0,SCM+FSA)) by SCMFSA8A:9;
A5: I c= I +* (Start-At (0,SCM+FSA)) by SCMFSA8A:9;
I +* (Start-At (0,SCM+FSA)) c= s2 +* (I +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
then A6: I c= s2 +* (I +* (Start-At (0,SCM+FSA))) by A4, XBOOLE_1:1;
I +* (Start-At (0,SCM+FSA)) c= s1 +* (I +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
then A7: I c= s1 +* (I +* (Start-At (0,SCM+FSA))) by A5, XBOOLE_1:1;

hereby :: thesis:

let k be Element of NAT ; :: thesis:
A8: IC (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),k)) in dom I by A1, SCMFSA7B:def 7;
I is_closed_on s2 by A1, A2, A3, SCMFSA8B:8;
then A9: for m being Element of NAT st m < k holds
IC (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),m)) in dom I by SCMFSA7B:def 7;
s1 +* (I +* (Start-At (0,SCM+FSA))),s2 +* (I +* (Start-At (0,SCM+FSA))) equal_outside NAT by A3, SCMFSA8B:7;
hence Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),k), Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),k) equal_outside NAT by A7, A6, A9, SCMFSA6B:21; :: thesis:
then A10: IC (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),k)) = IC (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),k)) by COMPOS_1:24;
I is_closed_on s2 by A1, A2, A3, SCMFSA8B:8;
then A11: IC (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),k)) in dom I by SCMFSA7B:def 7;
Y: (ProgramPart (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),k))) /. (IC (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),k))) = (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),k)) . (IC (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),k))) by COMPOS_1:38;
Z: (ProgramPart (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),k))) /. (IC (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),k))) = (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),k)) . (IC (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),k))) by COMPOS_1:38;
thus CurInstr ((ProgramPart (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),k))) = (s2 +* (I +* (Start-At (0,SCM+FSA)))) . (IC (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),k))) by Y, AMI_1:54
.= I . (IC (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),k))) by A6, A11, GRFUNC_1:8
.= (s1 +* (I +* (Start-At (0,SCM+FSA)))) . (IC (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),k))) by A7, A10, A8, GRFUNC_1:8
.= CurInstr ((ProgramPart (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),k))),(Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),k))) by Z, AMI_1:54 ; :: thesis:

end;