let s1, s2 be State of SCM+FSA ; :: thesis: for I being parahalting Program of SCM+FSA st I +* (Start-At 0 ,SCM+FSA ) c= s1 & I +* (Start-At 0 ,SCM+FSA ) c= s2 & s1,s2 equal_outside NAT holds
for k being Element of NAT holds
( Comput (ProgramPart s1),s1,k, Comput (ProgramPart s2),s2,k equal_outside NAT & CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,k)),(Comput (ProgramPart s2),s2,k) )
let I be parahalting Program of SCM+FSA ; :: thesis: ( I +* (Start-At 0 ,SCM+FSA ) c= s1 & I +* (Start-At 0 ,SCM+FSA ) c= s2 & s1,s2 equal_outside NAT implies for k being Element of NAT holds
( Comput (ProgramPart s1),s1,k, Comput (ProgramPart s2),s2,k equal_outside NAT & CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,k)),(Comput (ProgramPart s2),s2,k) ) )
assume that
A1: I +* (Start-At 0 ,SCM+FSA ) c= s1 and
A2: I +* (Start-At 0 ,SCM+FSA ) c= s2 and
A3: s1,s2 equal_outside NAT ; :: thesis: for k being Element of NAT holds
( Comput (ProgramPart s1),s1,k, Comput (ProgramPart s2),s2,k equal_outside NAT & CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,k)),(Comput (ProgramPart s2),s2,k) )
A4: I c= s2 by A2, Th5;
A5: I c= s1 by A1, Th5;

hereby :: thesis: verum

let k be Element of NAT ; :: thesis: ( Comput (ProgramPart s1),s1,k, Comput (ProgramPart s2),s2,k equal_outside NAT & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,k)),(Comput (ProgramPart s2),s2,k) = CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) )
A6: IC (Comput (ProgramPart s1),s1,k) in dom I by A1, Def2;
A7: IC (Comput (ProgramPart s2),s2,k) in dom I by A2, Def2;
for m being Element of NAT st m < k holds
IC (Comput (ProgramPart s2),s2,m) in dom I by A2, Def2;
hence Comput (ProgramPart s1),s1,k, Comput (ProgramPart s2),s2,k equal_outside NAT by A3, A5, A4, Th21; :: thesis: CurInstr (ProgramPart (Comput (ProgramPart s2),s2,k)),(Comput (ProgramPart s2),s2,k) = CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k)
then A8: IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) by COMPOS_1:24;
Y: (ProgramPart (Comput (ProgramPart s2),s2,k)) /. (IC (Comput (ProgramPart s2),s2,k)) = (Comput (ProgramPart s2),s2,k) . (IC (Comput (ProgramPart s2),s2,k)) by COMPOS_1:38;
Z: (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;
thus CurInstr (ProgramPart (Comput (ProgramPart s2),s2,k)),(Comput (ProgramPart s2),s2,k) = s2 . (IC (Comput (ProgramPart s2),s2,k)) by Y, AMI_1:54
.= I . (IC (Comput (ProgramPart s2),s2,k)) by A4, A7, GRFUNC_1:8
.= s1 . (IC (Comput (ProgramPart s1),s1,k)) by A5, A8, A6, GRFUNC_1:8
.= CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) by Z, AMI_1:54 ; :: thesis: verum

end;