Proposition 8

Let $E, F, G$ be three locally convex spaces; assume that $G$ is Hausdorff and quasi-complete. Let $E_0$ (resp. $F_0$) be a dense vector subspace of $E$ *(resp. $F$), $\mathfrak{S}_0$ (resp. $\mathfrak{T}_0$) a family of bounded subsets of $E_0$ (resp. $F_0$) such that every point of $E$ (resp. $F$) is in the closure of an element of $\mathfrak{S}_0$ (resp. $\mathfrak{T}_0$). Then every $(\mathfrak{S}_0, \mathfrak{T}_0)$*-hypocontinuous bilinear mapping* $u$ from $E_0 \times F_0$ into $G$ extends uniquely to a separately continuous bilinear mapping $\overline{u}$ from $E \times F$ into $G$ and $\overline{u}$ is $(\mathfrak{S}_0, \mathfrak{T}_0)$*-hypocontinuous*.

The uniqueness and hypocontinuity of $\overline{u}$ follows from prop. 7; it remains to prove the existence of $\overline{u}$. For every $y' \in F_0$, the continuous linear mapping $x' \mapsto u(x', y')$ from $E_0$ into $G$ extends uniquely to a continuous linear mapping $x \mapsto u_1(x, y')$ from $E$ into $G$ (III, p. 8, prop. 10). It follows immediately that for every $x \in E$, the mapping $y' \mapsto u_1(x, y')$ from $F_0$ into $G$ is linear; and we shall show that it is continuous. By hypothesis, there exists $M \in \mathfrak{S}_0$, such that $x \in \overline{M}$. For every closed neighbourhood $W$ of 0 in $G$, there exists, by hypothesis, a neighbourhood $V$ of 0 in $F_0$ such that $u(M \times V) \subset W$; since $x \mapsto u_1(x, y')$ is continuous, we deduce that $u_1(\overline{M} \times V) \subset W$, and in particular $u_1(x, y') \in W$ for all $y' \in V$. This establishes our assertion. By virtue of prop. 7, the bilinear map $u_1$ from $E \times F_0$ into $G$ is $(\mathfrak{S}_0, \mathfrak{T}_0)$*-hypocontinuous. We end the proof by interchanging the roles of $E$ and $F$ in the first part of the proof, applied to $u_1$.