let s1, s2 be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st I is_closed_on s1 & I is_halting_on s1 & I +* (Start-At (0,SCM+FSA)) c= s1 & I +* (Start-At (0,SCM+FSA)) c= s2 & ex k being Element of NAT st Comput ((ProgramPart s1),s1,k),s2 equal_outside NAT holds
Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT
set A = NAT ;
set D = Int-Locations \/ FinSeq-Locations;
let I be Program of SCM+FSA; :: thesis: ( I is_closed_on s1 & I is_halting_on s1 & I +* (Start-At (0,SCM+FSA)) c= s1 & I +* (Start-At (0,SCM+FSA)) c= s2 & ex k being Element of NAT st Comput ((ProgramPart s1),s1,k),s2 equal_outside NAT implies Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT )
assume A1: I is_closed_on s1 ; :: thesis: ( not I is_halting_on s1 or not I +* (Start-At (0,SCM+FSA)) c= s1 or not I +* (Start-At (0,SCM+FSA)) c= s2 or for k being Element of NAT holds not Comput ((ProgramPart s1),s1,k),s2 equal_outside NAT or Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT )
assume A2: I is_halting_on s1 ; :: thesis: ( not I +* (Start-At (0,SCM+FSA)) c= s1 or not I +* (Start-At (0,SCM+FSA)) c= s2 or for k being Element of NAT holds not Comput ((ProgramPart s1),s1,k),s2 equal_outside NAT or Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT )
assume A3: I +* (Start-At (0,SCM+FSA)) c= s1 ; :: thesis: ( not I +* (Start-At (0,SCM+FSA)) c= s2 or for k being Element of NAT holds not Comput ((ProgramPart s1),s1,k),s2 equal_outside NAT or Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT )
then A4: s1 = s1 +* (I +* (Start-At (0,SCM+FSA))) by FUNCT_4:79;
then A5: ProgramPart s1 halts_on s1 by A2, SCMFSA7B:def 8;
then consider n being Element of NAT such that
A6: CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,n))) = halt SCM+FSA by EXTPRO_1:30;
assume I +* (Start-At (0,SCM+FSA)) c= s2 ; :: thesis: ( for k being Element of NAT holds not Comput ((ProgramPart s1),s1,k),s2 equal_outside NAT or Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT )
then A7: s2 = s2 +* (I +* (Start-At (0,SCM+FSA))) by FUNCT_4:79;
given k being Element of NAT such that A8: Comput ((ProgramPart s1),s1,k),s2 equal_outside NAT ; :: thesis: Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT
set s3 = Comput ((ProgramPart s1),s1,k);
A9: IC SCM+FSA in dom (Comput ((ProgramPart s1),s1,k)) by COMPOS_1:9;
I c= I +* (Start-At (0,SCM+FSA)) by SCMFSA8A:9;
then I c= s1 by A3, XBOOLE_1:1;
then A10: I c= Comput ((ProgramPart s1),s1,k) by AMI_1:86;
IC (Comput ((ProgramPart s1),s1,k)) = IC s2 by A8, SCMFSA8A:6
.= IC ((s2 +* I) +* (Start-At (0,SCM+FSA))) by A7, FUNCT_4:15
.= 0 by FUNCT_4:121 ;
then (IC SCM+FSA) .--> 0 c= Comput ((ProgramPart s1),s1,k) by A9, FUNCOP_1:88;
then I +* (Start-At (0,SCM+FSA)) c= Comput ((ProgramPart s1),s1,k) by A10, FUNCT_4:92;
then A11: Comput ((ProgramPart s1),s1,k) = (Comput ((ProgramPart s1),s1,k)) +* (I +* (Start-At (0,SCM+FSA))) by FUNCT_4:79;

A12: now

let n be Element of NAT ; :: thesis: IC (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k)),n)) in dom I
T: ProgramPart (Comput ((ProgramPart s1),s1,k)) = ProgramPart s1 by AMI_1:123;
IC (Comput ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k)),n)) = IC (Comput ((ProgramPart s1),s1,(k + n))) by EXTPRO_1:5;
hence IC (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k)),n)) in dom I by A1, A4, T, SCMFSA7B:def 7; :: thesis: verum

end;

T: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,k)) by AMI_1:123;
x: Comput ((ProgramPart s1),s1,(n + k)) = Comput ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k)),n) by EXTPRO_1:5;
n <= n + k by NAT_1:11;
then yy: Comput ((ProgramPart s1),s1,(n + k)) = Comput ((ProgramPart s1),s1,n) by A6, EXTPRO_1:6;
CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k)),n))) = CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,(k + n)))) by x, T
.= CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,n))) by yy ;
then ProgramPart (Comput ((ProgramPart s1),s1,k)) halts_on Comput ((ProgramPart s1),s1,k) by A6, EXTPRO_1:30;
then A13: I is_halting_on Comput ((ProgramPart s1),s1,k) by A11, SCMFSA7B:def 8;
A14: DataPart (Comput ((ProgramPart s1),s1,k)) = DataPart s2 by A8, SCMFSA8A:6;
TX: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,k)) by AMI_1:123;
consider k being Element of NAT such that
A15: CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k))) = halt SCM+FSA by A5, EXTPRO_1:30;
TTX: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,k)) by AMI_1:123;
Y: (ProgramPart (Comput ((ProgramPart s1),s1,k))) /. (IC (Comput ((ProgramPart s1),s1,k))) = (Comput ((ProgramPart s1),s1,k)) . (IC (Comput ((ProgramPart s1),s1,k))) by COMPOS_1:38;
A16: (ProgramPart s1) . (IC (Comput ((ProgramPart s1),s1,k))) = s1 . (IC (Comput ((ProgramPart s1),s1,k))) by COMPOS_1:2
.= (Comput ((ProgramPart s1),s1,k)) . (IC (Comput ((ProgramPart s1),s1,k))) by AMI_1:54
.= (ProgramPart (Comput ((ProgramPart s1),s1,k))) /. (IC (Comput ((ProgramPart s1),s1,k))) by Y
.= (ProgramPart s1) /. (IC (Comput ((ProgramPart s1),s1,k))) by TTX
.= CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k)))
.= halt SCM+FSA by A15 ;
I is_closed_on Comput ((ProgramPart s1),s1,k) by A11, A12, SCMFSA7B:def 7;
then Result ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k))), Result ((ProgramPart s2),s2) equal_outside NAT by A7, A14, A11, A13, Th101;
hence Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT by A16, TX, EXTPRO_1:9; :: thesis: verum