diff --git a/src/cat/cat/universal.tex b/src/cat/cat/universal.tex
index 865c4be..d04caab 100644
--- a/src/cat/cat/universal.tex
+++ b/src/cat/cat/universal.tex
@@ -142,7 +142,7 @@ Let $\catc$ be a category and $(\seqi{A}, \bracsn{f^i_j| i, j \in I, i \lesssim
 \end{definition}
 
 \begin{proposition}
-\label{proposition:direct-limit}
+\label{proposition:module-direct-limit}
     Let $R$ be a ring and $(\seqi{A}, \bracsn{T^i_j| i, j \in I, i \lesssim j})$ be an upward-directed system of $R$-modules, then there exists $(A, \bracsn{T^i_A}_{i \in I})$ such that:
     \begin{enumerate}
         \item For each $i \in I$, $T^i_A \in \hom({A_i, A})$.
diff --git a/src/dg/derivative/mvt.tex b/src/dg/derivative/mvt.tex
index 3625394..f8b0f34 100644
--- a/src/dg/derivative/mvt.tex
+++ b/src/dg/derivative/mvt.tex
@@ -75,7 +75,7 @@
 
 
 \begin{theorem}[Mean Value Theorem]
-\label{theorem:mean-value-theorem}
+\label{theorem:mean-value-theorem-line}
     Let $-\infty < a < b < \infty$, $E$ be a separated locally convex space, $S \subset [a, b]$ be at most countable, and $f \in C([a, b]; E)$ be differentiable on $(a, b) \setminus N$, then
     \[
     f(b) - f(a) \in \overline{\text{Conv}\bracs{Df(x)(b - a)| x \in (a, b) \setminus N}}
@@ -84,7 +84,7 @@
 \begin{proof}
     By \ref{proposition:derivative-sets-real}, $f$ is right-differentiable on $(a, b) \setminus N$ with
     \[
-    D^+f(x) = Df(x) \in \bracs{Df(x)|x \in (a, b) \setminus N}
+    D^+f(x) = Df(x) \in \bracs{Df(y)|y \in (a, b) \setminus N}
     \]
     for all $x \in (a, b)$. Let $g(x) = x$, then by \ref{theorem:right-differentiable-convex-form},
     \[
@@ -92,16 +92,37 @@
     \]
 \end{proof}
 
+\begin{theorem}[Mean Value Theorem]
+\label{theorem:mean-value-theorem}
+    Let $E$ be a topological vector space, $F$ be a separated locally convex space, $V \subset E$ be open and star shaped at $x \in V$, $f: V \to F$ be Gateau-differentiable on $V$, then for any $y \in V$,
+    \[
+    f(y) - f(x) \in \overline{\text{Conv}\bracs{Df(z)(y - x)|z \in (x, y)}}
+    \]
+    where $[x, y] = \bracs{(1 - t)x + ty|y \in [0, 1]}$.
+\end{theorem}
+\begin{proof}
+    Let $g: [0, 1] \to F$ be defined by $g(t) = f((1 - t)x + ty)$. Since $f$ is Gateaux-differentiable, $g$ is differentiable by the chain rule \ref{proposition:chain-rule-sets-conditions} with $Dg(t) = Df((1 - t)x + ty)(y - x)$, and continuous by \ref{proposition:derivative-sets-real}.
+
+    By the Mean Value Theorem (\ref{theorem:mean-value-theorem-line}),
+    \[
+    f(y) - f(x) = g(1) - g(0) \in \overline{\text{Conv}\bracs{Dg(t)|t \in [0, 1]}} = \overline{\text{Conv}\bracs{Df(z)(y - x)|z \in (x, y)}}
+    \]
+\end{proof}
+
 \begin{proposition}
 \label{proposition:zero-derivative-constant}
     Let $E$ be a topological vector space, $F$ be a separated locally convex space, $V \subset E$ be open and connected, $f: V \to F$ be Gateaux-differentiable on $V$ such that $Df(x) = 0$ for all $x \in V$, then $f$ is constant.
 \end{proposition}
 \begin{proof}
-    Let $x, y \in V$ such that $\bracs{(1 - t)x + ty|t \in [0, 1]} \subset V$. Since $f$ is Gateaux-differentiable, $g: [0, 1] \to F$ defined by $g(t) = f((1 - t)x + ty)$ is differentiable with $Dg(t) = 0$ for all $t \in [0, 1]$. By the Mean Value Theorem (\ref{theorem:mean-value-theorem}), $f(y) - f(x) = 0$.
+    Let $x \in V$, then for any $U \in \cn(0)$ circled with $U + x \subset V$ and $y \in U + x$,
+    \[
+    f(y) - f(x) \in \overline{\text{Conv}\bracs{Df(z)(y - x)|z \in (x, y)}} = \bracs{0}
+    \]
+    by the Mean Value Theorem (\ref{theorem:mean-value-theorem-line}).
 
-    Fix $x \in V$ and let $W$ be the connected component of $\bracs{y \in V|f(x) = f(y)}$ containing $x$. Since $E$ is locally path-connected (\ref{proposition:tvs-locally-connected}), $W$ is open.
+    Fix $x \in V$ and let $W$ be the connected component of $\bracs{y \in V|f(x) = f(y)}$ containing $x$. For any $y \in W$, by \ref{proposition:tvs-good-neighbourhood-base}, there exists $U \in \cn(0)$ circled such that $U + y \subset V$. Therefore $W \supset W \cup (U + y)$, and $W$ is open by \ref{lemma:openneighbourhood}.
 
-    Let $y \in \overline{W}$. By \ref{proposition:tvs-good-neighbourhood-base}, there exists $U \in \cn_E(0)$ radial such that $U + y \subset V$. Since any point in $U$ is joined to $y$ via a line segment, $f$ is constant on $U + y$. As $y \in \overline{W}$, $U + y \cap W \ne \emptyset$, so $y \in W$.
+    For any $y \in \ol W \cap V$, there exists $U \in \cn(0)$ circled such that $U + y \subset V$. As $y \in \ol W \cap V$, $U \cap W \ne \emptyset$. Thus $f(y) = f(x)$, $y \in W$, and $W$ is relatively closed.
 
-    Since $W$ is both open and closed, $W$ must coincide with $V$.
+    Since $V$ is connected and $W \subset V$ is both open and closed, $W = V$.
 \end{proof}
diff --git a/src/dg/derivative/sets.tex b/src/dg/derivative/sets.tex
index a08d754..9d7333a 100644
--- a/src/dg/derivative/sets.tex
+++ b/src/dg/derivative/sets.tex
@@ -143,11 +143,12 @@
     Let $E$ be a separated topological vector space and $\sigma \subset B(\real)$ be an upward-directed system that contains finite sets, then
     \begin{enumerate}
         \item $\mathcal{R}_{\sigma}(\real; E) = \mathcal{R}_{B(\real)}(\real; E)$. Hence, all forms of $\sigma$-differentiability on $\real$ are equivalent.
-        \item For any $U \subset \real$ open, $f: U \to E$, and $x_0 \in U$, $f$ is ($\sigma$-)differentiable at $x_0$ if and only if
+        \item For any $U \subset \real$ open, $f: U \to E$, and $x_0 \in U$, $f$ is differentiable at $x_0$ if and only if
         \[
         \lim_{t \to 0}\frac{f(x + t) - f(x)}{t}
         \]
-        exists. In which case, the above limit is identified with the ($\sigma$-)derivative of $f$ at $0$.
+        exists. In which case, the above limit is identified with the derivative of $f$ at $0$.
+        \item For any $U \subset \real$ open, $f: U \to E$, and $x_0 \in U$, if $f$ is differentiable at $x_0$, then $f$ is continuous at $x_0$.
     \end{enumerate}
 \end{proposition}
 \begin{proof}