Set-theoretical description of the free product? There is something in the definition of the free product of two groups that annoys me, and it's this "word" thing:

If $G$ and $H$ are groups, a word in $G$ and $H$ is a product of the form
$$
    s_1 s_2 \dots s_m,
$$
where each $s_i$ is either an element of $G$ or an element of $H$. 

So what is this "word" guy? Does it come out of the blue? Does it come from some sort of new operation that I can perform with the two sets $G$ and $H$ -in addition to the well-known ones of union, intersection, Cartesian product...?
Fortunatelly, I think there is nothing new under the sun of set operations: it's easy to realise that words can be identified with elements of some Cartesian product (see below):
$$
(s_1, s_2, \dots , s_m )  \ .
$$
And Cartesian product is a well-established set-theoretical operation.
So I tried to translate the rest of Wikipedia's definition 

Such a word may be reduced using the following operations:
Remove an instance of the identity element (of either $G$ or $H$).
  Replace a pair of the form $g_1g_2$ by its product in $G$, or a pair $h_1h_2$ by its product in $H$.
Every reduced word is an alternating product of elements of $G$ and elements of $H$, e.g.
$$
 g_1 h_1 g_2 h_2 \dots g_r h_r.
 $$
The free product $G ∗ H$ is the group whose elements are the reduced words in $G$ and $H$, under the operation of concatenation followed by reduction.

in an elementary set setting. First, consider the set of "unreduced" tuples of elements of $G$ and $H$
$$
U =  G \sqcup H \sqcup (G\times G) \times (G\times H) \sqcup (H\times G) \sqcup (H\times H) \sqcup (G\times G \times G) \sqcup \dots 
$$
More concisely:

EDIT:
I think the following formula may be less messier than the one I wrote previously:
$$
U = \bigsqcup_{r \geq 1} (S_1 \times \cdots \times S_r),
$$
where $S_i = G$ or $S_i = H$.

So, elements of $U$ are ordered tuples (unreduced ones)
$$
(s_1, s_2, \dots , s_m),
$$
where each $s_i$ is either an element of $G$ or an element of $H$.
The product of two unreduced tuples is defined by concatenation
$$
(s_1, \dots , s_m) \cdot (t_1,  \dots , t_n) = (s_1, \dots , s_m, t_1 , \dots , t_n) \ .
$$
Now, consider the following equivalence relation in the set of unreduced tuples $U$:
$$
(s_1, s_2, \dots , s_{i-1}, 1, s_{i+1}, \dots , s_n) \sim (s_1, s_2, \dots, s_{i-1}, s_i, \dots , s_n) \ ,
$$
where $1$ is either the unit element of $G$ or the one of $H$. And
$$
(s_1, s_2, \dots , s_i,s_{i+1}, \dots , s_r) \sim (s_1, s_2, \dots , s_is_{i+1}, \dots , s_r )
$$
whenever two adjacent $s_i, s_{i+1} \in G$ or $s_i, s_{i+1} \in H$ at the same time. 
If you want, you may call the equivalence class of a tuple under this equivalence relation a reduced tuple. So every reduced tuple is an alternating one, 
$$
(g_1, h_1, \dots , g_r , h_r) \ ,
$$
with $g_i \in G$ and $h_i \in H$ for all $i = 1, \dots , r$.
Define the free product of $G$ and $H$ as the quotient:
$$
G*H = U/\sim \ .
$$
Finally, one verifies that concatenation is well-defined on unreduced tuples and gives $G*H$ a group structure.
After performing this elementary exercise I understand perfectly well why nobody defines the free product in this way, but I still wanted to ask:


*

*Is this correct?

*Is it written somewhere?

 A: In answer to your question about whether this is written somewhere: the construction of free products in my book Introduction to Topological Manifolds proceeds very much along these lines. (I'm not the only one who's written it down, but I don't have other references handy.) I don't go through the set-theoretic description of the set of ordered tuples in as much detail as you do, but it can be described more simply as just the disjoint union of the sets $(G\amalg H)^n$ over all n.  I like the concreteness of this construction as a way of giving one a handle on what the free product looks like.  Once the group is constructed, it's a relatively easy matter to prove after the fact that it is uniquely determined up to isomorphism as the coproduct in the category of groups.
A: You can see essentially the same construction in two different ways in George Bergman's An Invitation to General Algebra and Universal Constructions in Chapter 2 (link is to a postscript file) for the free group. 
First, you define "the set of all terms in the elements of the set $X$ under the formal group operations $\mu$, $i$, $e$" to mean a set which is given with functions symb${}_T\colon X\to T$, $\mu_T\colon T^2\to T$, $i_T\colon T\to T$, and $e_T\colon T^0\to T$, such that each of these maps is one-to-one, their images are disjoint, and $T$ is the union of the images, and $T$ is generated by symb${}_T(X)$ under the operations $\mu_T$, $i_T$, and $e_T$. Such a set exists (it can be constructed inductively with enough care; given in Chapter 1 of the same notes). Then one defines an apropriate equivalence relation $\sim$ on $T$; the set $T/\sim$ gives the underlying set of the free group, and one defines the operations in the free group via representatives in the natural way. Bergman labels this "the logician's approach" (section 2.2). 
An alternative construction ("the classical construction", section 2.4) gives "free groups as groups of words". Again, you start with a set $X$, and let $T$ be the set of all group-theoretic terms of $X$; identify $X$ with its image under symb, and one defines a subset $T_{red}$ of "reduced terms" (defining what this means appropriately) and then defining operations $\otimes$, ${}^{(-)}$, and $e_T$ on this set to make it into a group. Proving it is a group can be done either in the straightforward but tedious way, or by using "van der Waerden's trick" (embed the set $T_{red}$ into a group of permutations, and check that the operations you defined correspond to the operations in the image, so that "group"-ness gets inherited). 
To get the free product, you let $X$ be the disjoint union of the underlying sets of $G$ and $H$, and either adds to the equivalence relation (in the "logician's approach"), or restricts the definition of "reduced words" (in the "classical approach"), in essentially the way you did. 
A: In the question above, it seems that the description is far too complicated as it actually is. I will elaborate on the construction of coproducts of groups or monoids a bit. This will go beyond the scope of the specific question, but I hope it's helpful in other situations.
First assume $M,N$ are sets. What is their coproduct? Obviously it's the disjoint union, which I will denote by $M + N$. Now assume $M,N$ are monoids. What is their coproduct? Well we have to introduce products of elements in $M + N$. Thus consider $(M + N)^{<\omega}$, the set of finite sequences with entries in $M + N$. This is a monoid by concatenation, but the inclusions $M,N \to (M + N)^{<\omega}$ are no homomorphisms. Well, then let's force it! Mod out the smallest congruence relation $\sim$ on our monoid, which satisfies $1 \sim (1_M), (m,m') \sim (mm')$ for all $m,m' \in M$ and similarily for elements of $N$. Then the quotient $(M + N)^{<\omega} / \sim$ is obviously a monoid (since $\sim$ is a congruence relation), and the universal property of the coproduct is also verified easily.
Now what about groups? The correct definition of a group involves the operations of the underlying monoid and the inversion. But in practice, this inversion can be reconstructed from the rest of the data ($x=y^{-1}$ iff $xy=1$), and actually the category of groups is a full subcategory of the category of monoids. If the monoids $M,N$ above happen to be groups, their coproduct turns out to be a group, and clearly the universal property then also holds with respect to groups. Thus we have constructed the coproduct in the category of groups.
Let's turn back to monoids. The above construction of $M \coprod N$ is rather general, it shows the existence of colimits in every finitary algebraic category, but what can be said about the elements? Do they have a canonical representation? Now there are two ways of doing it:
a) The elegant, short, "geometric" one.
b) The long, tedious one. This one is preferred in textbooks ...
In our case, b) means that you write down the set of reduced words, endow it with a terribly complicated monoid structure, show that every monoid axiom is satisfied, and finally check the universal property. Good luck.
In a) you just use that $M \coprod N$ exists. We have constructed it, but the construction does not answer such simple questions as: Do $M$ and $N$ intersect in $M \coprod N$ trivially? Therefore we just use the existence of the coproduct together with the structure maps $i : M \to M \coprod N, j : N \to M \coprod N$. The idea is now to define an action of $M \coprod N$ on another object. This may be a geometric one, but in our case it's our desired set of reduced words.
Observe that the elements in $M \coprod N$, which are products of elements, which are in the image of $i$ or $j$, constitute a submonoid, which verifies the same universal property. In other words, every element in $M \coprod N$ is such a product. In such a product we may replace $i(m) i(m')$ by $i(mm')$ and cancel $i(1)$, similarily for $j$. Thus every element is in the image of the canonical map $X \to M \coprod N$, where
$X := \{(... ,m_1,n_1,m_2,n_2, ...)  : m_i \in M - \{1\}, n_i \in N - \{1\}\}.$
Now we prove that this map $X \to M \coprod N$ is a bijection, i.e. every element of the coproduct has a unique representation as $... i(m_1) j(n_1) i(m_2) ...$. To do this, we define an action of the monoid $M \coprod N$ on $X$, i.e. a monoid homomorphism $M \coprod N \to End(X), (m \mapsto (x \mapsto mx))$, which should imitate the usual multiplication. By the universal property, it is enough to construct this homomorphism on $M$ and on $N$. If $m \in M$ and $x \in X$, define $mx$ as follows: If $x$ starts with an element in $N$, just concatenate with $(m)$. If $x$ starts with an element of $M$, which is not inverse to $m$, then multiply $m$ in the first entry. Otherwise delete the first entry. Similarily the homomorphism $N \to End(X)$ is defined. The resultung homomorphism $M \coprod N \to End(X)$ can be composed with the evaluation at the empty sequence to get a map $M \coprod N \to X$, which turns out to be a left inverse to $X \to M \coprod N$. Thus, $X \to M \coprod N$ is a bijection.
A: Well, I think that the usual definition of the free product is just a slightly less formal version of what you've written, which, by the way, is certainly correct. I haven't seen it completely written out like that before but maybe others have.
Meanwhile, one can avoid the whole messy construction and prove (using, for example, a version of the adjoint functor theorem) that the category Grp has small colimits. The free product is just the coproduct in Grp, so that would suffice for all practical purposes, and it is a rigorous formulation, if that's what you're worried about.
A: This is not an answer to your questions, but I guess I would point out that the “words” in the definition in Wikipedia can be given a structure: consider the free monoid freely generated by the set $G \sqcup H$, and just call its elements words in G and H.  Now you can introduce an equivalence relation and define the free product as the quotient (similarly to what you did), verifying that the operation on the quotient is well-defined and makes it a group.
Of course, this is not at all shorter than your written-down definition if we write down the definition of the free monoid and the definition of the equivalence relation.  I just wanted to point out that the “words” are a natural concept and that this two-step construction may be slightly tidier than constructing the free product of groups in one big step (based on sets).
