\begin{definition}[Definition:Internal Group Direct Product/General Definition/Definition by Isomorphism]
Let $\sequence {H_n} = \struct {H_1, \circ {\restriction_{H_1} } }, \ldots, \struct {H_n, \circ {\restriction_{H_n} } }$ be a (finite) sequence of subgroups of a group $\struct {G, \circ}$
where $\circ {\restriction_{H_1} }, \ldots, \circ {\restriction_{H_n} }$ are the restrictions of $\circ$ to $H_1, \ldots, H_n$ respectively.
The group $\struct {G, \circ}$ is the '''internal group direct product of $\sequence {H_n}$''' {{iff}}:
:the mapping $\ds \phi: \prod_{k \mathop = 1}^n H_k \to G$ from the finite Cartesian product $\struct {H_1, \circ {\restriction_{H_1} } } \times \cdots \times \struct {H_n, \circ {\restriction_{H_n} } }$ to $\struct {G, \circ}$ defined as:
::$\ds \forall k \in \set {1, 2, \ldots, n}: \forall s_k \in H_k: \map \phi {h_1, \ldots, h_n} = \prod_{k \mathop = 1}^n h_k$
:is a group isomorphism.
\end{definition}