diff --git a/src/measure/measure/product.tex b/src/measure/measure/product.tex
index 9e2280d..c6e2f5f 100644
--- a/src/measure/measure/product.tex
+++ b/src/measure/measure/product.tex
@@ -127,7 +127,7 @@
 
     Therefore $\alg = \cm \otimes \cn$. 
 
-    Now let $F \subset L^+(X \times Y)$ be the set of functions satisfying (1), then $F \supset \Sigma^+(X, \cm)$ by linearity. Let $f \in L^+(X \times Y)$, then by \autoref{proposition:measurable-simple-separable}, there exists $\seq{\phi_n} \subset \Sigma^+(X \times Y)$ such that $\phi_n \upto f$. In which case, by the Monotone Convergence Theorem, (1) also holds for $f$. 
+    Now let $F \subset L^+(X \times Y)$ be the set of functions satisfying (1), then $F \supset \Sigma^+(X, \cm)$ by linearity. Let $f \in L^+(X \times Y)$, then by \autoref{lemma:measurable-simple-separable}, there exists $\seq{\phi_n} \subset \Sigma^+(X \times Y)$ such that $\phi_n \upto f$. In which case, by the Monotone Convergence Theorem, (1) also holds for $f$. 
 \end{proof}