Theorem: Duality Mapping of Dual System is Jointly Continuous when Dual Restricted to Absolute Polar of Open Neighborhood of Origin

Let $\GF \in \set {\R, \C}$.
Let $\innerprod E F$ be a dual system over $\GF$.
Let $\tau$ be a locally convex topology on $E$ consistent with $\innerprod E F$.
Let $\map \sigma {F, E}$ be the weak-$\ast$ topology induced by $\innerprod E F$.
Let $V$ be an open neighborhood of ${\mathbf 0}_E$ in $\struct {E, \tau}$. 
Let $V^\circ$ be the absolute polar of $V$.
Let $\struct {E, \tau} \times \struct {F, \map \sigma {F, E} }$ be the direct product of $\struct {E, \tau}$ and $\struct {F, \map \sigma {F, E} }$ with the product topology.
Define $\innerprod \cdot \cdot : \struct {E, \tau} \times \struct {V^\circ, \map \sigma {F, E} } \to \GF$ by:
:$\innerprod x f = \map f x$ for each $\tuple {x, f} \in E \times V^\circ$.
Then $\innerprod \cdot \cdot$ is continuous.

Proof:
We use Characterization of Continuity in terms of Nets.
Let $\struct {\Lambda, \preceq}$ be a directed set.
Let $\family {\tuple {x_\lambda, f_\lambda} }_{\lambda \mathop \in \Lambda}$ be a net in $E \times V^\circ$ converging to $\struct {x, f}$.
We aim to show that $\innerprod {x_\lambda} {f_\lambda} \to \innerprod x f$.
From Characterization of Convergence of Net in Product Topology, we have:
:$x_\lambda \to x$ in $\struct {E, \tau}$
and:
:$f_\lambda \to f$ in $\struct {F, \map \sigma {F, E} }$.
We can write:
{{begin-eqn}}
{{eqn	| l = \size {\innerprod {x_\lambda} {f_\lambda} - \innerprod x f}
		| r = \size {\innerprod {x_\lambda} {f_\lambda} - \innerprod x {f_\lambda} + \innerprod x {f_\lambda} - \innerprod x f}
}}
{{eqn	| o = \le
		| r = \size {\innerprod {x_\lambda} {f_\lambda} - \innerprod x {f_\lambda} } + \size {\innerprod x {f_\lambda} - \innerprod x f}
		| c = Triangle Inequality
}}
{{eqn	| r = \size {\innerprod {x_\lambda - x} {f_\lambda} } + \size {\innerprod x {f_\lambda} - \innerprod x f}
		| c = {{Defof|Dual System}}
}}
{{end-eqn}}
Let $\epsilon > 0$. 
From Dilation of Open Set in Topological Vector Space is Open, $\frac \epsilon 2 V$ is an open neighborhood of ${\mathbf 0}_E$ in $\struct {E, \tau}$.
Hence, since $x_\lambda \to x$, there exists $\lambda_0 \in \Lambda$ such that:
:$\ds x_\lambda - x \in \frac \epsilon 2 V$ for each $\lambda \in \Lambda$ with $\lambda \succeq \lambda_0$.
Hence we can write:
:$\ds x_\lambda - x = \frac \epsilon 2 u_\lambda$ for $u_\lambda \in V$.
We have:
{{begin-eqn}}
{{eqn	| l = \innerprod {x_\lambda - x} {f_\lambda}
		| r = \innerprod {\frac \epsilon 2 u_\lambda} {f_\lambda} 
}}
{{eqn	| r = \frac \epsilon 2 \innerprod {u_\lambda} {f_\lambda} 
		| c = {{Defof|Dual System}}
}}
{{end-eqn}}
Since $u_\lambda \in V$ and $f_\lambda \in V^\circ$, we have:
:$\ds \size {\innerprod {u_\lambda} {f_\lambda} } \le 1$
from the definition of the absolute polar. 
Hence we have:
:$\ds \size {\innerprod {x_\lambda} {f_\lambda} - \innerprod x {f_\lambda} } \le \frac \epsilon 2$ for $\lambda \succeq \lambda_0$.
From Characterization of Convergence of Net in Weak-* Topology Induced by Dual System, we have:
:$\innerprod x {f_\lambda} \to \innerprod x f$ 
Hence there exists $\lambda_0' \in \Lambda$ such that:
:$\ds \size {\innerprod x {f_\lambda} - \innerprod x f} < \frac \epsilon 2$ for $\lambda \succeq \lambda_0'$.
Since $\struct {\Lambda, \preceq}$ is directed, there exists $\lambda_1 \in \Lambda$ with $\lambda_1 \succeq \lambda_0$ and $\lambda_1 \succeq \lambda_0$.
Then for $\lambda \in \Lambda$ with $\lambda \succeq \lambda_1$, we have:
:$\ds \size {\innerprod {x_\lambda} {f_\lambda} - \innerprod x {f_\lambda} } \le \frac \epsilon 2$
and:
:$\ds \size {\innerprod x {f_\lambda} - \innerprod x f} < \frac \epsilon 2$ 
Hence:
:$\size {\innerprod {x_\lambda} {f_\lambda} - \innerprod x f} < \epsilon$ for $\lambda \succeq \lambda_1$.
Since $\epsilon$ was arbitrary, we have:
:$\innerprod {x_\lambda} {f_\lambda} \to \innerprod x f$
Hence by Characterization of Continuity in terms of Nets, $\innerprod \cdot \cdot : \struct {E, \tau} \times \struct {V^\circ, \map \sigma {F, E} } \to \GF$ is continuous.
{{qed}}