User:IssaRice/Computability and logic/Rogers fixed point theorem using Sipser's notation

Sipser's textbook presents the recursion theorem, but not the fixed point theorem. Here is one way to state the fixed point theorem using Sipser's notation.

Theorem (Fixed point theorem). Let $F$ be a Turing machine which computes a function $f:{\mathrm{\Sigma }}^{*}\to {\mathrm{\Sigma }}^{*}$. Then there exists a Turing machine $T$ which computes a function $t:{\mathrm{\Sigma }}^{*}\to {\mathrm{\Sigma }}^{*}$, and a Turing machine $R$ which computes a function $r:{\mathrm{\Sigma }}^{*}\to {\mathrm{\Sigma }}^{*}$, such that $f(⟨T⟩)=⟨R⟩$ and $t(w)=r(w)$ for all $w\in {\mathrm{\Sigma }}^{*}$.