Definition 12

The group with operators $G = \prod_{i \in I} G_i$ defined above is the product group with operators of the $G_i$. The mappings $\mathrm{pr}_i : G \to G_i$ are called the projection homomorphisms.

A particular case of the product of groups with operators is the group $G^E$ consisting of the mappings of a set $E$ into a group with operators $G$, the laws being defined by:

Let $(\phi_i : H \to G_i)_{i \in I}$ be a family of homomorphisms of groups with operators. The mapping $h \mapsto (\phi_i(h))_{i \in I}$ of $H$ into $\prod_{i \in I} G_i$ is a homomorphism of groups with operators. It is the only homomorphism $\Phi : H \to \prod_{i \in I} G_i$ satisfying $\mathrm{pr}_i \circ \Phi = \phi_i$ for all $i$. This justifies the name "product group with operators" (Set Theory, IV, § 2, no. 4).

Let $(\phi_i : H_i \to G_i)_{i \in I}$ be a family of homomorphisms of groups with operators. The mapping $\prod_{i \in I} \phi_i : (h_i)_{i \in I} \mapsto (\phi_i(h_i))_{i \in I}$ of $\prod_{i \in I} H_i$ into $\prod_{i \in I} G_i$ is a homomorphism of groups with operators.