Incremental update.

src/fa/rs/rs-bv.tex

@@ -24,18 +24,18 @@
 \label{proposition:rs-complete}
     Let $[a, b] \subset \real$, $E_1, E_2, H$ be locally convex spaces, and $E_1 \times E_2 \to H$ with $(x, y) \mapsto xy$ be a continuous bilinear map, and $G \in BV([a, b]; E_2)$.
 
-    For each continuous seminorm $\rho$ on $H$ and $f: [a, b] \to E$, define
+    For each continuous seminorm $\rho$ on $E_1$ and $f: [a, b] \to E_1$, define
     \[
-    [f]_{u, \rho} = \sup_{x \in [a, b]}f(\rho)
+    [f]_{u, \rho} = \sup_{x \in [a, b]}\rho(f(x))
     \]
     Let $\net{f} \subset RS([a, b], G)$ such that:
     \begin{enumerate}
-        \item[(a)] $\rho(f_\alpha - f) \to 0$ for all continuous seminorm $\rho$ on $E_1$.
+        \item[(a)] For each continuous seminorm $\rho$ on $E_1$, $[f_\alpha - f]_{u, \rho} \to 0$.
         \item[(b)] $\lim_{\alpha \in A}\int_a^b f_\alpha dG$ exists.
     \end{enumerate}
     then $f \in RS([a, b], G)$ and $\int_a^b f dG = \lim_{\alpha \in A}\int_a^b f_\alpha dG$. In particular,
     \begin{enumerate}
-        \item If $H$ is complete, then condition (a) may be omitted.
+        \item If $H$ is complete, then condition (b) may be omitted.
         \item If $H$ is sequentially complete and $A = \nat^+$, then condition (b) may be omitted.
     \end{enumerate}
 \end{proposition}