The union of the two groups involved in a free product is not quite disjoint $-$ they have to share the same identity element. But otherwise yes, $G*H$ is the free group on $G\cup H$ modulo $1_G=1_H$ and the multiplication tables already in place for $G$ and $H$. Indeed if $G=\langle X|R\rangle$ and $H=\langle Y|S\rangle$ are presentations with $X,Y$ disjoint (by fiat) then $G*H=\langle X\cup Y|R\cup S\rangle$.
In the category of abelian groups the coproduct is the direct sum. This can be obtained from the free product by imposing commutativity: (assuming $G,H$ commutative) we can interpret $G,H$ themselves as subgroups of $G*H$, and we have $G\oplus H= (G*H)/[G,H]$. This is indeed the most free abelian group generated by $G\cup H$ (modulo $1_G=1_H$).
In general, if $\mathcal{A}$ is a variety of algebras and $U : \mathcal{A} \to \mathbf{Sets}$ is the forgetful functor, then we can construct a left adjoint $F : \mathbf{Sets} \to \mathcal{A}$ as follows:
First, take the set of formal expressions built up from atoms corresponding to elements of $X$, using formal counterparts of the operations in $\mathcal{A}$. (If you're using ZFC as your foundations, you will likely need a set-theoretic argument to show this can be represented by an actual set rather than a proper class.)
Then, take the quotient by the smallest equivalence relation which contains all instances of relations in $\mathcal{A}$ with formal expressions substituted in, and which also makes all the formal operations be respectful of the equivalence relation. (It is straightforward to show the class of relations on the set of formal expressions from (1) satisfying these requirements is closed under arbitrary intersections; so then, for example, you could construct the desired equivalence relation as the intersection of all such relations.)
Then, in many cases, it's possible to represent each equivalence class by a member of a restricted class of expressions which is easier to work with; and if we're lucky, we might even be able to choose a canonical such expression in each equivalence class.
In the case $\mathcal{A} = \mathbf{Groups}$, for example, it is easy to show that any formal expression from (1), modulo the equivalence relation in (2), is equivalent to a (possibly empty) product of elements $x \in X$ or $y^{-1}$ for $y \in X$ which together form a reduced word. You would prove this by "structural induction" on the general formal expression (or, if you prefer, by strong induction on the "total size" of the general formal expression). The harder part is to show that any two distinct
reduced words end up in different equivalence classes.
To make this process more concrete in the group case, I think it might help to show how this would be encoded in Coq, where for example (1) is very similar to the way you would define an "abstract syntax tree" type in OCaml or Haskell:
(* formal expressions from (1) *)
Inductive free_group (X:Type) : Type :=
| fg_atom (x:X)
| fg_id
| fg_inv (x : free_group X)
| fg_mul (x y : free_group X).
Arguments fg_atom [X] x.
Arguments fg_id [X].
Arguments fg_inv [X] x.
Arguments fg_mul [X] x y.
(* Equivalence relation described in (2) *)
Inductive fg_equiv (X:Type) : free_group X -> free_group X -> Prop :=
| fg_left_id : forall x : free_group X,
fg_equiv X (fg_mul fg_id x) x
| fg_right_id : forall x : free_group X,
fg_equiv X (fg_mul x fg_id) x
| fg_left_inv : forall x : free_group X,
fg_equiv X (fg_mul (fg_inv x) x) fg_id
| fg_right_inv : forall x : free_group X,
fg_equiv X (fg_mul x (fg_inv x)) fg_id
| fg_mul_assoc : forall x y z : free_group X,
fg_equiv X (fg_mul (fg_mul x y) z) (fg_mul x (fg_mul y z))
| fg_equiv_refl : forall x : free_group X,
fg_equiv X x x
| fg_equiv_sym : forall x y : free_group X,
fg_equiv X x y -> fg_equiv X y x
| fg_equiv_trans : forall x y z : free_group X,
fg_equiv X x y -> fg_equiv X y z -> fg_equiv X x z
| fg_equiv_resp_id : fg_equiv X fg_id fg_id
| fg_equiv_resp_inv : forall x x' : free_group X,
fg_equiv X x x' -> fg_equiv X (fg_inv x) (fg_inv x')
| fg_equiv_resp_mul : forall x x' y y' : free_group X,
fg_equiv X x x' -> fg_equiv X y y' ->
fg_equiv X (fg_mul x y) (fg_mul x' y').
(Incidentally, it's also very easy to extend this to describe the group with any given presentation, or in general the object of any variety of algebras with a given presentation: just add the relations from the presentation to the requirements on the equivalence relation in (2).)
Best Answer
What Lang shows is that if the groups are infinite cyclic then their free product is a free group. But that's because the infinite cyclic group is itself free.
The free product of an arbitrary family of groups can be defined similarly to how the free product of a finite family is defined. But in general it will not be free.
Recall that a subgroup of a free group is necessarily free. Thus we have:
Theorem. Let $\{G_i\}_{i\in I}$ be a family of groups. The free product $\mathop{*}\limits_{i\in I}G_i$ is a free group if and only if each $G_i$ is free.
Proof. Since the free product contains a copy of each $G_i$, if the free product is free, then each $G_i$ is free.
Conversely, if $G_i$ is free on $X_i$, then the free product is free on $X = \mathop{\amalg}\limits_{i\in I} X_i$, the disjoint union of the $X_i$: given any set map $f\colon X\to K$ from $X$ to (the underlying set of) a group $K$, this map corresponds to a family of maps $f_i\colon X_i\to K$, and each $X_i$ induces a morphism $F_i\colon G_i\to K$ with $F_i|_{X_i}=f$. The universal property of the free product then induces a morphism $F\colon\mathop{*}\limits_{i\in I}G_i\to K$ with $F\ circ\iota_j= F_j$ for each $j$ (where $\iota_j$ is the embedding of $G_j$ into the free product. Thus, $F\circ\iota_j|_{X_j} = f_j$, and thus the restriction of $F$ to (the image of) $X$ is equal to $f$. Thus, the free product has the relevant universal property and hence is the free group on $X$. $\Box$