Definition 11.7.2 (Locally Convex Direct Sum).label Let $\seqi{E}$ be locally convex spaces over $K \in \RC$, then there exists $(E, \seqi{\iota})$ such that:
- (1)
$E$ is a locally convex space over $K$.
- (2)
For each $i \in I$, $\iota_{i} \in L(E_{i}; E)$.
- (U)
For each $(F, \seqi{T})$ satisfying (1) and (2), there exists a unique $T \in L(E; F)$ such that the following diagram commutes:
\[\xymatrix{ A \ar@{->}[r]^{T} & B \\ A_i \ar@{->}[u]^{\iota_i} \ar@{->}[ru]_{T_i} & }\] - (4)
The family
\[\fB = \bracs{\Gamma\paren{\bigcup_{i \in I}\iota_i(U_i)} \bigg | U_i \in \cn_{E_i}(0)}\]is a fundamental system of neighbourhoods for $E$ at $0$.
The space $E = \bigoplus_{i \in I}E_{i}$ is the locally convex direct sum of $\seqi{E}$.
Proof. Let $(E, \seqi{\iota})$ be the direct sum of $\seqi{E}$ as vector spaces, and equip it with the inductive topology induced by $\seqi{\iota}$, then $(E, \seqi{\iota})$ satisfies (1) and (2).
(U): By (U) of the direct sum, there exists a unique $T \in \hom(E; F)$ such that the diagram commutes. In which case, by (4) of Definition 11.7.1, $T \in L(E; F)$.
(4): By (6) of Definition 11.7.1.$\square$