diff --git a/src/measure/measurable-maps/approx.tex b/src/measure/measurable-maps/approx.tex
new file mode 100644
index 0000000..2317052
--- /dev/null
+++ b/src/measure/measurable-maps/approx.tex
@@ -0,0 +1,162 @@
+\section{Approximations with Simple Functions}
+\label{section:simple-approx}
+
+\begin{definition}[Admissible Approximant Function]
+\label{definition:admissible-approximant-function}
+    Let $X$ be a topological space and $\mathcal{A}: X \to 2^X$, then $\mathcal{A}$ is an \textbf{admissible approximant function} on $X$ if:
+    \begin{enumerate}[label=(AA\arabic*)]
+        \item For each $x \in X$, $x \in \overline{\mathcal{A}(x)^o}$. 
+        \item $\bigcap_{x \in X}\mathcal{A}(x) \ne \emptyset$. 
+    \end{enumerate}
+
+    and $\mathcal{A}$ is \textbf{Borel measurable} if:
+    \begin{enumerate}[label=(AA\arabic*), start=2]
+        \item[(B)] For any $x_0 \in X$, $\bracs{x \in X|x_0 \in \mathcal{A}(x)} \in \cb_X$.
+    \end{enumerate}
+\end{definition}
+
+\begin{lemma}
+\label{lemma:admissible-approximant-existence}
+    Let $X$ be a topological space, and $\mathcal{A}: X \to 2^X$ be defined by $x \mapsto X$, then $\mathcal{A}$ is an \hyperref[admissible approximant function]{definition:admissible-approximant-function}. 
+\end{lemma}
+
+
+\begin{definition}[Approximation of the Identity]
+\label{definition:approximation-id-measure}
+    Let $X$ be a topological space, $\mathcal{A}: X \to 2^X$ be an \hyperref[admissible approximant function]{definition:admissible-approximant-function} and $\net{I} \subset X^X$ be a net, then $\net{I}$ is an \textbf{$\mathcal{A}$-admissible approximation of the identity} if:
+    \begin{enumerate}[label=(AI\arabic*)]
+        \item For each $x \in X$, $I_\alpha(x) \to x$. 
+        \item For each $x \in X$ and $\alpha \in A$, $I_\alpha(x) \in \mathcal{A}(x)$. 
+    \end{enumerate}
+
+    The approximation $\net{I}$ is \textbf{simple} if $I_\alpha$ is finitely-valued for all $\alpha \in A$, and \textbf{Borel measurable} if $I_\alpha$ is Borel measurable for all $\alpha \in A$. 
+\end{definition}
+
+\begin{lemma}[Existence of Simple Approximations of the Identity]
+\label{lemma:separable-metric-space-approx-identity}
+    Let $X$ be a separable metric space, $\mathcal{A}: X \to 2^X$ be a Borel measurable \hyperref[admissible approximant function]{definition:admissible-approximant-function}, and $\seq{x_n} \subset X$ be a dense subset with $x_1 \in \bigcap_{x \in X}\mathcal{A}(x)$, then there exists $\seq{I_n} \subset X^X$ such that:
+    \begin{enumerate}
+        \item $\seq{I_n}$ is an $\mathcal{A}$-admissible \hyperref[approximation of the identity]{definition:approximation-id-measure}. 
+        \item For each $N \in \natp$, $I_N$ is Borel measurable with $I_N(X) \subset \bracsn{x_n|1 \le n \le N}$. 
+    \end{enumerate}
+\end{lemma}
+\begin{proof}
+    By removing duplicate elements from the sequence, assume without loss of generality that for each $m, n \in \natp$ with $m \ne n$, $x_m \ne x_n$. 
+
+    Let $N \in \natp$. For each $x \in X$, let
+    \[
+    C_N(x) = \bracs{1 \le n \le N| x_n \in \mathcal{A}(x)}
+    \]
+
+    Since $x_1 \in \bigcap_{y \in X}\mathcal{A}(y)$, $1 \in C_N(x)$ and $C_N(x) \ne \emptyset$. 
+    
+    From here, let
+    \[
+    k_N(x) = \min\bracs{n \in C_N(x) \bigg | d(x, x_n) = \min_{m \in C_N(x)}d(x, x_m)}
+    \]
+
+    be the minimum $n \in C_N(x)$ on which the minimal distance from $x$ to $\bracs{x_m|m \in C_N(x)}$ is achieved. Then, for each $n \in \natp$, 
+    \begin{align*}
+        \bracs{k_N \le n} &= \bigcup_{j = 1}^n \bracs{x \in X \bigg | j \in C_N(x), d(x, x_j) = \min_{m \in C_N(x)}d(x, x_m)} \\
+        &= \bigcup_{j = 1}^n \bracs{j \in C_N} \cap \bracs{x \in X \bigg | d(x, x_j) = \min_{m \in C_N(x)}d(x, x_m)} \\
+        &= \bigcup_{j = 1}^n\bigcup_{J \subset [N]} \bracs{j \in C_N, J = C_N} \cap \bracs{x \in X \bigg | d(x, x_j) = \min_{m \in J}d(x, x_m)} 
+    \end{align*}
+
+    Given that $\mathcal{A}$ is Borel measurable, $\bracs{n \in C_N} = \bracs{x_n \in \mathcal{A}(x)}$ is a Borel set for each $1 \le n \le N$. As a result, $\bracs{J = C_N}$ is Borel for each $J \subset [N]$. Thus $\bracs{j \in C_N, J = C_N}$ is Borel for each $1 \le j \le n$ and $J \subset [N]$. 
+
+    On the other hand, for each $1 \le n \le N$, the function $x \mapsto d(x, x_n)$ is continuous and hence Borel measurable. Similarly, for each $J \subset [N]$, the mapping $\real^J \to \real$ with $\alpha \mapsto \min_{j \in J}\alpha_j$ is also Borel measurable. 
+    
+    
+    The above facts combined show that $\bracs{k_N \le n}$ is a Borel set, and $k_N: X \to [N]$ is a Borel measurable function. Now, let
+    \[
+    I_N: X \to \bracsn{x_n|1 \le n \le N} \quad x \mapsto x_{k_N(x)}
+    \]
+
+    then for each $1 \le n \le N$, $\bracs{I_N = x_n} = \bracs{k_N = n}$ is a Borel set. Thus $I_N$ is Borel measurable. 
+
+    In addition, for each $x \in X$, $k_N(x) \in C_N(x)$, so
+    \[
+    I_N(x) = x_{k_N(x)} \in \bracs{x_n|n \in C_N(x)} \subset \mathcal{A}(x)
+    \]
+
+    and $\seq{I_N}$ satisfies (AI2).
+
+    Finally, for each $x \in X$ and $\eps > 0$, since $x \in \ol{\mathcal{A}(x)^o}$, there exists $N_0 \in \natp$ such that $x_{N_0} \in \mathcal{A}(x)$ and $d(x, x_{N_0}) < \eps$. In which case, for any $N \ge N_0$, $N_0 \in C_N(x)$ and $d(x, I_N(x)) \le d(x, x_{N_0}) < \eps$. Thus $I_N(x) \to x$ as $N \to \infty$, and $\seq{I_N}$ satisfies (AI1). 
+    
+    Therefore $\seq{I_N}$ is an approximation of the identity satisfying (1) and (2). 
+\end{proof}
+
+
+
+\begin{corollary}
+\label{corollary:measurable-simple-separable}
+    Let $(X, \cm)$ be a measurable space, $Y$ be a separable metric space, and $\mathcal{A}: Y \to 2^Y$ be a Borel measurable \hyperref[admissible approximant function]{definition:admissible-approximant-function}, then for any $f: X \to Y$, the following are equivalent:
+    \begin{enumerate}
+        \item $f$ is $(\cm, \cb_Y)$-measurable.
+        \item For any dense subset $\seq{y_n} \subset Y$ with $y_1 \in \bigcap_{y \in Y}\mathcal{A}(y)$, there exists a sequence $\seq{f_n}$ of $(\cm, \cb_Y)$-measurable simple functions such that
+        \begin{enumerate}
+            \item[(i)] For each $x \in X$ and $N \in \natp$,
+            \[
+            f_N(x) \in \mathcal{A}(f(x)) \cap \bracsn{y_n|1 \le n \le N}
+            \]
+            \item[(ii)] $f_n \to f$ pointwise as $n \to \infty$.
+        \end{enumerate}
+
+        \item There exists a sequence $\seq{f_n}$ of $(\cm, \cb_Y)$-measurable simple functions such that $f_n \to f$ pointwise.
+    \end{enumerate}
+\end{corollary}
+\begin{proof}
+    (1) $\Rightarrow$ (2): Let $\seq{y_n} \subset Y$ be a dense subset with $y_1 \in \bigcap_{y \in Y}\mathcal{A}(y)$. By \autoref{lemma:separable-metric-space-approx-identity}, there exists $\seq{I_n} \subset Y^Y$ such that:
+    \begin{enumerate}
+        \item $\seq{I_n}$ is an $\mathcal{A}$-admissible \hyperref[approximation of the identity]{definition:approximation-id-measure}. 
+        \item For each $N \in \natp$, $I_N$ is Borel measurable with $I_N(Y) \subset \bracsn{y_n|1 \le n \le N}$. 
+    \end{enumerate}
+
+    For each $n \in \natp$, let $f_n = I_N \circ f_n$, then:
+    \begin{enumerate}
+        \item[(i)] For each $x \in X$ and $N \in \natp$,
+        \[
+        f_N(x) = I_N(f(x)) \in \mathcal{A}(f(x)) \cap \bracsn{y_n|1 \le n \le N}
+        \]
+        \item[(ii)] Since $I_n \to \text{Id}$ pointwise as $n \to \infty$, $f_n \to f$ pointwise as $n \to \infty$. 
+    \end{enumerate}
+
+    (3) $\Rightarrow$ (1): By \autoref{proposition:metric-measurable-limit}.
+\end{proof}
+
+\begin{corollary}
+\label{corollary:measurable-simple-separable-norm}
+    Let $(X, \cm)$ be a measurable space, $(E, \norm{\cdot}_E)$ be a separable normed vector space, and $f: X \to E$, then the following are equivalent:
+    \begin{enumerate}
+        \item $f$ is $(\cm, \cb_E)$-measurable.
+        \item There exists simple functions $\seq{f_n}$ such that $\abs{f_n} \le \abs{f}$ for all $n \in \natp$, and $f_n \to f$ pointwise.
+    \end{enumerate}
+\end{corollary}
+\begin{proof}
+    (1) $\Rightarrow$ (2): Let
+    \[
+    \mathcal{A}: E \to 2^E \quad y \mapsto \begin{cases}
+        B_E(0, \norm{y}_E) & y \ne 0 \\ 
+        E & y = 0
+    \end{cases}
+    \]
+
+    then
+    \begin{enumerate}
+        \item[(AA1)] For each $y \in E$, $y \in \ol{\mathcal{A}(y)^o}$.
+        \item[(AA2)] $0 \in \bigcap_{y \in E}\mathcal{A}(y)$.
+        \item[(B)] For any fixed $y_0 \in E \setminus \bracs{0}$,
+        \[
+        \bracs{y \in E|y_0 \in \mathcal{A}(y)} = \bracs{y \in E|\norm{y_0}_E < \norm{y}_E} \cup \bracs{0} \in \cb_E
+        \]
+
+        and $\bracs{y \in E|0 \in \mathcal{A}(y)} = E$. 
+    \end{enumerate}
+
+    so $\mathcal{A}$ is a Borel measurable \hyperref[admissible approximant function]{definition:admissible-approximant-function}. 
+
+    By (2) of \autoref{corollary:measurable-simple-separable}, there exists simple functions $\seq{f_n}$ such that $|f_n| \le |f|$ on $\bracs{f \ne 0}$ for all $n \in \natp$ and $f_n \to f$ pointwise. In which case, $|\one_{\bracs{f \ne 0}}f_n| \le |f|$ globally for all $n \in \natp$ and $\one_{\bracs{f \ne 0}}f_n \to f$ pointwise as $n \to \infty$. 
+
+    (2) $\Rightarrow$ (1): By \autoref{proposition:metric-measurable-limit}.
+\end{proof}
+
diff --git a/src/measure/measurable-maps/index.tex b/src/measure/measurable-maps/index.tex
index a56100f..1ef3fd3 100644
--- a/src/measure/measurable-maps/index.tex
+++ b/src/measure/measurable-maps/index.tex
@@ -6,4 +6,5 @@
 \input{./real-valued.tex}
 \input{./simple.tex}
 \input{./metric.tex}
+\input{./approx.tex}
 \input{./in-measure.tex}
diff --git a/src/measure/measurable-maps/metric.tex b/src/measure/measurable-maps/metric.tex
index cf1920b..13ad1a9 100644
--- a/src/measure/measurable-maps/metric.tex
+++ b/src/measure/measurable-maps/metric.tex
@@ -21,7 +21,7 @@
 
 \begin{proposition}
 \label{proposition:metric-measurables}
-    Let $(X, \cm)$ be a measurable space, $Y$ be a metrisable topological space, $f, g: X \to Y$ be $(\cm, \cb_Y)$-measurable functions, then the following functions are measurable:
+    Let $(X, \cm)$ be a measurable space, $Y$ be a separable and metrisable topological space, $f, g: X \to Y$ be $(\cm, \cb_Y)$-measurable functions, then the following functions are measurable:
     \begin{enumerate}
         \item For any metric $d$ on $Y$, $x \mapsto d(f(x), f(y))$.
         \item If $Y$ is a TVS over $K \in \RC$ and $\lambda \in K$, $\lambda f + g$. In particular, $\bracs{f = g} \in \cm$.
@@ -69,92 +69,3 @@
 \end{proof}
 
 
-\begin{lemma}
-\label{lemma:measurable-simple-separable}
-    Let $(X, \cm)$ be a measurable space, $Y$ be a separable metric space, and $\mathcal{A}: Y \to 2^Y$ such that
-    \begin{enumerate}
-        \item[(a)] For each $y \in Y$, $y \in \ol{\mathcal{A}(y)^o}$.
-        \item[(b)] $\bigcap_{y \in Y}\mathcal{A}(y) \ne \emptyset$.
-        \item[(c)] For any $y_0 \in Y$, $\bracs{y \in Y|y_0 \in \mathcal{A}(y)} \in \cb_Y$.
-    \end{enumerate}
-
-    Then, for any $f: X \to Y$, the following are equivalent:
-    \begin{enumerate}
-        \item $f$ is $(\cm, \cb_Y)$-measurable.
-        \item For any dense subset $\seq{y_n} \subset Y$ with $y_1 \in \bigcap_{y \in Y}\mathcal{A}(y)$, there exists a sequence $\seq{f_n}$ of $(\cm, \cb_Y)$-measurable simple functions such that
-        \begin{enumerate}
-            \item[(i)] For each $x \in X$ and $N \in \natp$, $f_N(x) \in \mathcal{A}(f(x)) \cap \bracsn{y_n|1 \le n \le N}$.
-            \item[(ii)] $f_n \to f$ pointwise.
-        \end{enumerate}
-
-        \item There exists a sequence $\seq{f_n}$ of $(\cm, \cb_Y)$-measurable simple functions such that $f_n \to f$ pointwise.
-    \end{enumerate}
-\end{lemma}
-\begin{proof}
-    (1) $\Rightarrow$ (2): Let $\seq{y_n} \subset Y$ be a dense subset with $y_1 \in \bigcap_{y \in Y}\mathcal{A}(y)$. For each $N \in \natp$ and $x \in X$, define
-    \[
-    C(N, x) = \bracs{1 \le n \le N|y_n \in \mathcal{A}(f(x))}
-    \]
-
-    Since $y_1 \in \bigcap_{y \in Y}\mathcal{A}(y)$, $1 \in C(N, x) \ne \emptyset$. Let
-    \[
-    k(N, x) = \min\bracs{n \in C(N, x) \bigg | d(f(x), y_n) = \min_{m \in C(N, x)}d(f(x), y_m)}
-    \]
-
-    then for any $k \in \natp$, $\bracs{x \in X|k(N, x) \le k}$ is equal to
-    \[
-     \bigcup_{j = 1}^k\bracs{x \in X \bigg |j \in C(N, x), d(f(x), y_j) = \min_{m \in C(N, x)}d(f(x), y_m)}
-    \]
-
-    For each $1 \le m \le N$, $y \mapsto d(y, y_m)$ is continuous. Thus $x \mapsto d(f(x), y_m)$ and $x \mapsto \min_{m \in C(N, x)}d(f(x), y_m)$ are $(\cm, \cb_\real)$-measurable by \autoref{proposition:limit-measurable} and assumption (c). By \autoref{proposition:metric-measurables},
-    \[
-    \bracs{x \in X \bigg | d(f(x), y_j) = \min_{m \in C(N, x)}d(f(x), y_m)} \in \cm
-    \]
-
-    for each $1 \le j \le k$. Combining this with assumption (c) shows that $\bracs{x \in X|k(N, x) \le k} \in \cm$.
-
-    Let $f_N(x) = y_{k(N, x)}$, then for each $N \in \natp$, $f_N(X) \subset \bracs{y_n|1 \le n \le N}$. Since $x \mapsto k{(N, x)}$ is $(\cm, 2^\natp)$-measurable, $f_N$ is $(\cm, \cb_Y)$-measurable.
-
-    Fix $x \in X$, then
-    \[
-    f(x) \in \ol{\mathcal{A}(f(x))^o} = \ol{\bracs{y_n| n \in \natp, y_n \in \mathcal{A}(f(x))^o}}
-    \]
-
-    by assumption (a) and \autoref{definition:dense}. Thus for any $\eps > 0$, there exists $N \in \natp$ such that $y_N \in \mathcal{A}(f(x))^o$ and $d(f(x), y_N) < \eps$. In which case, $d(f(x), f_n(x)) < \eps$ for all $n \ge N$. Therefore $f_n \to f$ pointwise.
-
-    (3) $\Rightarrow$ (1): By \autoref{proposition:metric-measurable-limit}.
-\end{proof}
-
-\begin{corollary}
-\label{corollary:measurable-simple-separable-norm}
-    Let $(X, \cm)$ be a measurable space, $(E, \norm{\cdot}_E)$ be a separable normed vector space, and $f: X \to E$, then the following are equivalent:
-    \begin{enumerate}
-        \item $f$ is $(\cm, \cb_E)$-measurable.
-        \item There exists simple functions $\seq{f_n}$ such that $\abs{f_n} \le \abs{f}$ for all $n \in \natp$, and $f_n \to f$ pointwise.
-    \end{enumerate}
-\end{corollary}
-\begin{proof}
-    (1) $\Rightarrow$ (2): Let
-    \[
-    \mathcal{A}: E \to 2^E \quad y \mapsto \begin{cases}
-        B_E(0, \norm{y}_E) & y \ne 0 \\ 
-        E & y = 0
-    \end{cases}
-    \]
-
-    then
-    \begin{enumerate}
-        \item[(a)] For each $y \in E$, $y \in \ol{\mathcal{A}(y)^o}$.
-        \item[(b)] $0 \in \bigcap_{y \in E}\mathcal{A}(y)$.
-        \item[(c)] For any fixed $y_0 \in E \setminus \bracs{0}$,
-        \[
-        \bracs{y \in E|y_0 \in \mathcal{A}(y)} = \bracs{y \in E|\norm{y_0}_E < \norm{y}_E} \cup \bracs{0} \in \cb_E
-        \]
-
-        and $\bracs{y \in E|0 \in \mathcal{A}(y)} = E$. 
-    \end{enumerate}
-
-    By (2) of \autoref{lemma:measurable-simple-separable}, there exists simple functions $\seq{f_n}$ such that $|f_n| \le |f|$ on $\bracs{f \ne 0}$ for all $n \in \natp$ and $f_n \to f$ pointwise. In which case, $|\one_{\bracs{f \ne 0}}f_n| \le |f|$ globally for all $n \in \natp$ and $\one_{\bracs{f \ne 0}}f_n \to f$ pointwise. 
-
-    (2) $\Rightarrow$ (1): By \autoref{proposition:metric-measurable-limit}.
-\end{proof}
diff --git a/src/measure/measure/localisable.tex b/src/measure/measure/localisable.tex
index 0c46ad3..87cb741 100644
--- a/src/measure/measure/localisable.tex
+++ b/src/measure/measure/localisable.tex
@@ -103,3 +103,67 @@
 \end{proof}
 
 
+\begin{lemma}
+\label{lemma:gluing-measurable-sets}
+    Let $(X, \cm, \mu)$ be a localisable measure space, $\cf = \bracs{A \in \cm|\mu(A) < \infty}$, $\bracs{(E_A, F_A)}_{A \in \cf}$ such that:
+    \begin{enumerate}[label=(\alph*)]
+        \item For each $A \in \cf$, $E_A, F_A \in \cm$, $E_A, F_A \subset A$, and $E_A \cap F_A = \emptyset$. 
+        \item For each $A, B \in \cf$, $\mu((E_A \cap B) \Delta (E_B \cap A)) = 0$ and $\mu((F_A \cap B) \Delta (F_B \cap A)) = 0$.
+    \end{enumerate}
+
+    Let $E$ and $F$ be essential suprema of $\bracsn{E_A}_{A \in \cf}$ and $\bracsn{F_A}_{A \in \cf}$, respectively, then
+    \begin{enumerate}
+        \item For each $B \in \cf$, $\mu(E \cap F_B) = 0$. 
+        \item $\mu(E \cap F) = 0$.
+    \end{enumerate}
+\end{lemma}
+\begin{proof}
+    (1): Let $A, B \in \cf$, then
+    \begin{align*}
+        \mu(E_A \setminus F_B^c) &= \mu(E_A \cap F_B) = \mu(E_A \cap F_B \cap A \cap B) \\
+        &\le \mu(E_A \cap F_A) + \mu((F_A \cap B) \Delta F_B \cap A \cap B) = 0
+    \end{align*}
+
+    so $F_B^c$ is an essential upper bound of $\bracs{E_A}_{A \in \cf}$. Since $E$ is an essential supremum of $\bracs{E_A}_{A \in \cf}$, $\mu(E \setminus F_B^c) = \mu(E \cap F_B) = 0$. 
+    
+    (2): For any $B \in \cf$, $\mu(F_B \setminus E^c) = \mu(F_B \cap E) = \mu(E \cap F_B) =0$. Thus $E^c$ is an essential upper bound of $\bracs{F_B}_{B \in \cf}$. Given that $F$ is an essential supremum of $\bracsn{F_B}_{B \in \cf}$, $\mu(F \cap E) = \mu(F \setminus E^c) = 0$. 
+\end{proof}
+
+
+\begin{lemma}[Gluing Lemma for Measurable Functions]
+\label{lemma:gluing-measurable}
+    Let $(X, \cm, \mu)$ be a localisable measure space, $\cf = \bracs{A \in \cm|\mu(A) < \infty}$, $Y$ be a Polish space, and $\bracsn{f_A: A \to Y|A \in \cf}$ such that:
+    \begin{enumerate}[label=(\alph*)]
+        \item For each $A \in \cf$, $f_A \in \mathcal{L}^0(A; Y)$. 
+        \item For each $A, B \in \cf$, $f_A|_{A \cap B} = f_B|_{A \cap B}$ almost everywhere.  
+    \end{enumerate}
+    
+    then there exists $f: X \to Y$ such that:
+    \begin{enumerate}
+        \item $f \in \mathcal{L}^0(X; Y)$. 
+        \item For each $A \in \cf$, $f|_A = f_A$ almost everywhere. 
+        \item[(U)] For any $g: X \to Y$ satisfying (1) and (2), $f = g$ almost everywhere. 
+    \end{enumerate}
+\end{lemma}
+\begin{proof}
+    First suppose that $Y$ is finite. For each $y \in Y$, let $P(y)$ be an essential supremum of $\bracs{f_A^{-1}(y)|A \in \cf}$. By \autoref{lemma:gluing-measurable-sets}, for any $x, y \in Y$ with $x \ne y$, $\mu(P(x) \cap P(y)) = 0$. After modification by null sets, assume without loss of generality that $X = \bigsqcup_{y \in Y}P(y)$. 
+
+    For each $x \in X$, let $f(x) \in Y$ be the unique element of $Y$ such that $x \in P(f(x))$, then:
+    \begin{enumerate}
+        \item For each $y \in Y$, $f^{-1}(y) = P(y)$, so $f \in \mathcal{L}^0(X; Y)$ is measurable. 
+        \item Let $A \in \cf$, then for each $y \in Y$, $\mu(f_A^{-1}(y) \setminus P(y)) = 0$. On the other hand, 
+        \begin{align*}
+         (P(y) \cap A) \setminus f_A^{-1}(y) &= P(y) \cap \bigcup_{z \in Y \setminus \bracs{y}}f_A^{-1}(z) \\
+         &\subset \braks{P(y) \cap \bigcup_{z \in Y \setminus \bracs{y}}P(z)} \cup \bigcup_{z \in Y \setminus \bracs{y}}f_A^{-1}(z) \setminus P(z)
+        \end{align*}
+
+        is a null set. Therefore $f|_A = f_A$ almost everywhere. 
+        \item For all $A \in \cf$, $f|_A = g|_A$ almost everywhere. Since $\mu$ is semifinite, $f = g$ almost everywhere. 
+    \end{enumerate}
+    
+    Therefore $f$ is the desired function. 
+
+    Now suppose that $Y$ is arbitrary. Let $\seq{y_n} \subset Y$ be a dense subset of $Y$. By \autoref{corollary:measurable-simple-separable}, for each
+\end{proof}
+
+
diff --git a/src/measure/measure/product.tex b/src/measure/measure/product.tex
index c6e2f5f..bab03c4 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{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$. 
+    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{corollary: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}