\begin{array}{c} \begin{array}{l} \left[\forall_{k \in \{0~\ldotp \ldotp~2^{t} - 1\}}~\left(\left({_{t}}\langle m \rvert \thinspace {\mathrm {FT}}^{\dag}_{t} \thinspace \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi \cdot k} \cdot \lvert k \rangle_{t}\right)\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi \cdot k} \cdot \left({_{t}}\langle m \rvert \thinspace {\mathrm {FT}}^{\dag}_{t} \thinspace \lvert k \rangle_{t}\right)\right)\right)\right] \Rightarrow \\ \left(\begin{array}{c} \begin{array}{l} \left[k \mapsto \left\{{_{t}}\langle m \rvert \thinspace {\mathrm {FT}}^{\dag}_{t} \thinspace \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi \cdot k} \cdot \lvert k \rangle_{t}\right) \textrm{ if } k \in \{0~\ldotp \ldotp~2^{t} - 1\}\right..\right] = \\ \left[k \mapsto \left\{\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi \cdot k} \cdot \left({_{t}}\langle m \rvert \thinspace {\mathrm {FT}}^{\dag}_{t} \thinspace \lvert k \rangle_{t}\right) \textrm{ if } k \in \{0~\ldotp \ldotp~2^{t} - 1\}\right..\right] \end{array} \end{array}\right) \end{array} \end{array}