A general way to see that such inductive definitions are well-founded is to observe that the definitions may be understood as defining a least fixed point of a monotone operator. This approach works for any sort of deductive systems, including ones that have several kinds of judgments, and even for infinitary ones.
Let us first consider a simple example where there is no mutual induction, for instance provability of formulas in first-order logic. Let $F$ be the set of all formulas (or all strings, if you suspect that even the notion of a well-formed formula is susupect) and suppose we would like to define the subset $T \subseteq F$ of all provable formulas. Inference rules are all of the form
$$\frac{Q_1 \quad Q_2 \quad \cdots \quad Q_n}{P}$$
which we read as
"If premises $P_1, \ldots, P_n$ are provable then conclusion $Q$ is provable."
Define the set $I$ of all instances of all inference rules whose elements are pairs $(\{Q_1, \ldots, Q_n\}, P)$ where $Q_1, \ldots, Q_n, P \in F$ and there is some inference rule which allows us to conclude from premises $Q_1, \ldots, Q_n$ that $P$. (Note: typically an inference rule is a schema which has many instances. We put these instances in $I$.)
We will exhibit $T$ as the least fixed point of a monotone operator $C : P(F) \to P(F)$ where $P(F)$ is the powerset of $F$. The operator $C$ is defines as
$$C(S) = \{ P \in F \mid \exists Q_1, \ldots, Q_n \in S .
(\{Q_1, \ldots, Q_n\}, P) \in I\}.$$
It is easy to check that $C$ is monotone and that therefore by Tarski's fixed point theorem it has a least fixed point $T$. The set $T$ is precisely the set of all derivable formulas that we are after.
We may allow infinitary inference rules of the form
$$\frac{Q_1 \quad Q_2 \quad Q_n \quad \cdots}{P}$$
and nothing much changes, except that the elements of $I$ are now of the form $(Q, P)$ where $Q$ is an arbitrary set of premises, rather than a finite one. Tarski's fixed point theorem still applies, although it gets harder to compute the fixed point by iteration (we have to go transfinite up the ordinals).
We might face a mutually inductive definition, say of types and terms. The situation is only slightly more complicated in such a case. We deal with two sets of syntactic entities, $F_\mathrm{term}$ and $F_\mathrm{type}$, and two monotone operators $$C_\mathrm{term} : P(F_\mathrm{term}) \times P(F_\mathrm{type}) \to P(F_\mathrm{term})$$
and
$$C_\mathrm{type} : P(F_\mathrm{term}) \times P(F_\mathrm{type}) \to P(F_\mathrm{type}).$$
Tarski's fixed-point theorem still applies because we can combine these into a single monotone operator $$C = \langle C_\mathrm{term}, C_\mathrm{type} \rangle : P(F_\mathrm{term}) \times P(F_\mathrm{type}) \to P(F_\mathrm{term}) \times P(F_\mathrm{type}).$$
The least fixed point $(T_\mathrm{term}, T_\mathrm{type})$ gives both terms and types simultaneously.
One may also observe that a product of powers is isomorphic to a power of a sum,
$$P(F_\mathrm{term}) \times P(F_\mathrm{type}) \cong P(F_\mathrm{term} + F_\mathrm{type})$$
and reduce the mutually inductive case back to the ordinary one.
One may object that I am shooting a sparrow with a cannon ball. Do we really need general powersets and Tarski's fixed-point theorem? Well, yes if we want to show that in general there is never a problem. In a specific case a lesser fixed point theorem will suffice. For instance, all formal systems that occur in practice are finitary and the set $I$ is primitive recursive, so a fairly weak induction principle on natural numbers will suffice to establish the existence of a least fixed point.
