Definition 5.2.5 (Product Uniformity). Let $\bracs{(X_i, \fU_i)}_{i \in I}$ be a family of uniform spaces, then the product uniformity $\fU$ on $X = \prod_{i \in I}X_{i}$ is the initial uniformity generated by the projections $\seqi{\pi}$, and:
The family
\[\fB = \bracs{\bigcap_{j \in J}(\pi_j \times \pi_j)^{-1}(U_j) \bigg | J \subset I \text{ finite}, U_j \in \fU_j}\]forms a fundamental system of entourages for $\fU$.
For any uniform space $(Y, \mathfrak{V})$ and $\seqi{f}$ where $f_{i} \in UC(Y; X_{i})$ for all $i \in I$, there exists a unique $f \in UC(Y; X)$ such that the following diagram commutes
\[\xymatrix{ Y \ar@{->}[d]_{f} \ar@{->}[rd]^{f_i} & \\ X \ar@{->}[r]_{\pi_i} & X_i }\]for all $i \in I$.
Proof. (1): By (3) of Definition 5.2.3.
(U): Let $f = \prod_{i \in I}f_{i}$, then $f: Y \to X$ is the unique function such that the diagram commutes for all $i \in I$.
For each $J \subset I$ finite and $\bigcap_{j \in J}(\pi_{j} \times \pi_{j})^{-1}(U_{j}) \in \fU$,
by (F2) of $\mathfrak{V}$.$\square$