Definition of Internal Group Direct Product - how does it follow that $(a,b) \circ (c,d) = (a \circ c, b \circ d)$? In my quest to build up a full understanding of the Internal Direct Product in the context of more-or-less general algebraic structures of $1$ operation, I am struggling with the following.
We are given the following definition:
Let $A$ and $B$ be closed subsets of an algebraic structure of one operation $(S, \circ)$.
Consider the mapping $\phi: A \times B \to S$ defined as:
$$\forall (a, b) \in A \times B: \phi (a, b) = a \circ b$$
Then $(S, \circ)$ is the internal direct product of $(A, \circ)$ and $(B, \circ)$ if and only if $\phi$ is an isomorphism.
(This definition is in Seth Warner's "Modern Algebra" (1965), Section 13.)
He then goes on to state and (IMO dubiously) prove that if $H$ and $K$ are subgroups of a group $G$, then the above definition holds if and only if:

*

*

*

*Every element of $H$ commutes with every element of $K$



*


*$H \circ K = G$



*


*$H \cap K = \{e\}$ (where $e$ is the identity of $G$)



2 and 3 are clear and obvious.
However, I have a problem with 1.
First thing Warner does is say:
"If $x \in H$ and if $y \in K$, then $(e, y) \circ (x, e) = (x, y)$."
Where does that come from?
From what I can tell, this comes from the unstated but assumed identity:
$$\forall (h_1, k_1), (h_2, k_2) \in H \times K: (h_1, k_1) \circ (h_2, k_2) = (h_1 \circ h_2, k_1 \circ k_2)$$
Where is that justified?
We can of course justify the assumption that $\forall (h_1, k_1), (h_2, k_2) \in H \times K: (h_1, k_1) \circ (h_2, k_2) = (h_1 \circ k_1, h_2 \circ k_2)$, which follows directly from the definition of $\phi$ and the assumption that one can go there from $\phi((h_1,k_1)\circ(h_2,k_2)) = \phi(h_1 \circ k_1, h_2 \circ k_2)$.
But from what I can tell, the only way you can get $(h_1, k_1) \circ (h_2, k_2) = (h_1 \circ h_2, k_1 \circ k_2)$ is by assuming it.
But if this is so, it cannot be the case that the only defining criterion of an internal direct product is that the abovedefined $\phi$ is an isomorphism.
Can anyone help me with this: where does that $(h_1, k_1) \circ (h_2, k_2) = (h_1 \circ h_2, k_1 \circ k_2)$ come from?
Is it just that because "internal direct product" has the name "direct product" in it, then it is "taken for granted" that it has the same property as the external direct product, which is defined on the cartesian product of $2$ unrelated groups $G \times H$ such that $\forall (g_1, h_1), (g_2, h_2) \in G \times H: (g_1, h_1)(g_2, h_2) = (g_1 g_2, h_1 h_2)$?
I'm sorry to keep banging on about this, but I haven't been able to get anyone to understand the nature of my confusion so far.
 A: Right, so I believe I have answered my question myself.
Let me restate what it is Warner said, this time being careful to be as thorough as possible (paraphrasing into standard terminology and notation as we go).

Let $A$ and $B$ be closed subsets of an algebraic structure of $1$ operation $(S, \circ)$. The algebraic structure $(S, \circ)$ is the internal direct product of $A$ and $B$ if the mapping $\phi$ from $A \times B$ to $S$ defined by:
$$\phi: (x, y) \to x \circ y$$
is an isomorphism from the cartesian product of $(A, \circ_A)$ and $(B, \circ_B)$ onto $(S, \circ)$."

So, what I missed about this the first time (and second, third and $n$th times) I read it is:
cartesian product of $(A, \circ_A)$ and $(B, \circ_B)$
which is defined 2 pages earlier as follows:

Let $(A, \circ_1)$ and $(B, \circ_2)$ be algebraic structures. The operation induced on $A \times B$ by $\circ_1$ and $\circ_2$ is the operation $\circ$ defined by:
$$(x_1, y_1) \circ (x_2, y_2) = (x_1 \circ_1 x_2, y_1 \circ_2 y_2)$$
for all $(x_1, y_1), (x_2, y_2) \in A \times B$. The algebraic structure $(A \times B, \circ)$ is called the cartesian product of $(A, \circ_1)$ and $(B, \circ_2)$.

So there you have it.
Buried deep in the definition of the internal direct product (which he calls the direct composite) is that sneaky definition of cartesian product, which I have been referring to as the external direct product as far as I can remember.
Thus, in Warner's exposition, the cartesian product of two structures is not only the set of ordered pairs of elements of the factors, but also the operation on those ordered pairs which go to make up that set.
Many thanks to all who have watched me hack away at this stubborn bit of metaphorical undergrowth, and take the advice that a brisk walk in the sunshine is just the thing to resharpen one's intellectual machete.
