diff --git a/src/op/system/complete-upgrade.tex b/src/op/system/complete-upgrade.tex
index 856891d..76e5568 100644
--- a/src/op/system/complete-upgrade.tex
+++ b/src/op/system/complete-upgrade.tex
@@ -191,7 +191,7 @@ The following is a slight generalisation of one form of the above example, but s
         \]
     \end{enumerate}
 \end{lemma}
-\begin{proof}
+\begin{proof}[Proof, {{\cite[Lemma 3.13]{Paulsen}}}. ]
     Since $P \ge 0$, there exists $\bracsn{a_{j, k}}_{j, k = 1}^n$ such that
     \begin{align*}
     P &= \braks{\sum_{j, k = 1}^n E_{jk} \otimes a_{j, k}}^*\braks{\sum_{j, k = 1}^n E_{jk} \otimes a_{j, k}} \\
@@ -235,11 +235,11 @@ The following is a slight generalisation of one form of the above example, but s
     \phi(E_{ij}) = \sum_{k = 1}^n b_{k, i}^* b_{k, j}
     \]
 
-    For each $1 \le k \le n$, let $S_k = \sum_{l = 1}^n E_{kl} \otimes a_{k, l}^*$. Let $1 \le i, j \le n$, then
+    For each $1 \le k \le n$, let $S_k = \sum_{l = 1}^n E_{kl} \otimes b_{k, l}^*$. Let $1 \le i, j \le n$, then
     \begin{align*}
-    \sum_{k = 1}^n S_k (E_{ij} \otimes 1_B) S_k^* &= \sum_{k = 1}^n \sum_{s, t = 1}^n (E_{ks} \otimes a_{k, s}^*) (E_{ij} \otimes 1_B) (E_{kt} \otimes a_{k, t}^*)^* \\
-    &= \sum_{k = 1}^n \sum_{s, t = 1}^n (E_{ks} \otimes a_{k, s}^*) (E_{ij} \otimes 1_B) (E_{tk} \otimes a_{k, t}) \\
-    &= \sum_{k = 1}^n E_{kk} \otimes a_{k, i}^* a_{k, j}^* = \sum_{k = 1}^n E_{kk} \otimes \phi(E_{ij})
+    \sum_{k = 1}^n S_k (E_{ij} \otimes 1_B) S_k^* &= \sum_{k = 1}^n \sum_{s, t = 1}^n (E_{ks} \otimes b_{k, s}^*) (E_{ij} \otimes 1_B) (E_{kt} \otimes b_{k, t}^*)^* \\
+    &= \sum_{k = 1}^n \sum_{s, t = 1}^n (E_{ks} \otimes b_{k, s}^*) (E_{ij} \otimes 1_B) (E_{tk} \otimes b_{k, t}) \\
+    &= \sum_{k = 1}^n E_{kk} \otimes b_{k, i}^* b_{k, j}^* = \sum_{k = 1}^n E_{kk} \otimes \phi(E_{ij})
     \end{align*}
 
     By linearity, for each $T \in M_n(\complex)$,