\begin{array}{c} \begin{array}{l} \left[\forall_{k}~\left(\left\{\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi \cdot k} \cdot \lvert k \rangle \textrm{ if } k \in \{0 + 1~\ldotp \ldotp~1\}\right.. = \left\{\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi \cdot k} \cdot \lvert k \rangle \textrm{ if } k \in \{1~\ldotp \ldotp~1\}\right..\right)\right] \Rightarrow \\ \left(\begin{array}{c} \begin{array}{l} \left[k \mapsto \left\{\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi \cdot k} \cdot \lvert k \rangle \textrm{ if } k \in \{0 + 1~\ldotp \ldotp~1\}\right..\right] = \\ \left[k \mapsto \left\{\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi \cdot k} \cdot \lvert k \rangle \textrm{ if } k \in \{1~\ldotp \ldotp~1\}\right..\right] \end{array} \end{array}\right) \end{array} \end{array}