[proofplan]
The defining sum $\operatorname{Ind}^G_H \psi(g) = \frac{1}{|H|}\sum_{x \in G} \mathring{\psi}(x^{-1} g x)$ runs over all of $G$, but $G$ partitions into the $|G:H| = n$ left cosets $t_1 H, \ldots, t_n H$. We rewrite the sum as a double sum over $i \in \{1, \ldots, n\}$ and $h \in H$ via the unique decomposition $x = t_i h$. The key identity $\mathring{\psi}(h^{-1}(t_i^{-1} g t_i) h) = \mathring{\psi}(t_i^{-1} g t_i)$ — valid because $\mathring{\psi}$ is constant on $H$-conjugacy classes both inside $H$ (by class-functionality of $\psi$) and outside $H$ (where it is zero) — collapses the inner sum over $h$ to $|H|$ identical terms, cancelling the $\frac{1}{|H|}$ prefactor.
[/proofplan]
[step:Decompose every $x \in G$ uniquely as $x = t_i h$ using the left transversal]
Let $t_1, \ldots, t_n$ be a left transversal of $H$ in $G$, where $n = |G : H|$. By definition of a left transversal, the cosets $t_1 H, t_2 H, \ldots, t_n H$ partition $G$:
\begin{align*}
G = \bigsqcup_{i=1}^n t_i H.
\end{align*}
Hence every $x \in G$ admits a unique decomposition
\begin{align*}
x = t_i h, \qquad i \in \{1, \ldots, n\}, \quad h \in H.
\end{align*}
The map
\begin{align*}
\{1, \ldots, n\} \times H &\to G \\
(i, h) &\mapsto t_i h
\end{align*}
is therefore a bijection.
[/step]
[step:Reindex the defining sum as a double sum over $(i, h)$]
By the definition of [Induced Class Function](/theorems/2447),
\begin{align*}
\operatorname{Ind}^G_H \psi(g) = \frac{1}{|H|} \sum_{x \in G} \mathring{\psi}(x^{-1} g x).
\end{align*}
Substituting $x = t_i h$ and using the bijection from Step 1, the sum over $x \in G$ becomes a double sum over $(i, h) \in \{1, \ldots, n\} \times H$:
\begin{align*}
\operatorname{Ind}^G_H \psi(g) = \frac{1}{|H|} \sum_{i=1}^n \sum_{h \in H} \mathring{\psi}\bigl((t_i h)^{-1}\, g\, (t_i h)\bigr).
\end{align*}
The argument of $\mathring{\psi}$ simplifies algebraically:
\begin{align*}
(t_i h)^{-1}\, g\, (t_i h) = h^{-1} t_i^{-1} g\, t_i h = h^{-1} (t_i^{-1} g\, t_i)\, h.
\end{align*}
So
\begin{align*}
\operatorname{Ind}^G_H \psi(g) = \frac{1}{|H|} \sum_{i=1}^n \sum_{h \in H} \mathring{\psi}\bigl(h^{-1} (t_i^{-1} g\, t_i)\, h\bigr).
\end{align*}
[/step]
[step:Show $\mathring{\psi}$ is invariant under $H$-conjugation, i.e., $\mathring{\psi}(h^{-1} y h) = \mathring{\psi}(y)$ for all $y \in G$, $h \in H$]
Fix $h \in H$ and $y \in G$. We split into two cases according to whether $y \in H$.
**Case 1: $y \in H$.** Then $h^{-1} y h \in H$ as well (since $H$ is a subgroup closed under multiplication and inversion). By definition of the zero extension,
\begin{align*}
\mathring{\psi}(h^{-1} y h) = \psi(h^{-1} y h) = \psi(y) = \mathring{\psi}(y),
\end{align*}
where the middle equality uses that $\psi \in \mathcal{C}(H)$ is a class function on $H$, hence constant on $H$-conjugacy classes.
**Case 2: $y \in G \setminus H$.** Then $h^{-1} y h \in G \setminus H$ as well. Indeed, if $h^{-1} y h$ were in $H$, then $y = h(h^{-1} y h)h^{-1}$ would be a product of elements of $H$, hence in $H$ — contradicting $y \notin H$. By definition of the zero extension,
\begin{align*}
\mathring{\psi}(h^{-1} y h) = 0 = \mathring{\psi}(y).
\end{align*}
In both cases, $\mathring{\psi}(h^{-1} y h) = \mathring{\psi}(y)$.
[guided]
The class function $\psi$ is defined on $H$, and $\mathring{\psi}$ extends it by zero outside $H$. We must check that the extension is invariant under conjugation by elements of $H$ (not by all of $G$ — that would generally fail). The two cases reflect a structural fact: conjugation by $h \in H$ preserves the partition $G = H \sqcup (G \setminus H)$.
**Why does $H$-conjugation preserve $H$?** For $y \in H$, the product $h^{-1} y h$ involves three elements of $H$, hence lies in $H$ by closure. For $y \notin H$, the contrapositive: if $h^{-1}yh \in H$, then $y = h(h^{-1}yh)h^{-1} \in H$ — but $y \notin H$, contradiction. So $H$ and $G \setminus H$ are each $H$-conjugation-stable.
**Why does $\psi$ being an $H$-class function suffice?** Inside $H$, the values of $\mathring{\psi}$ are values of $\psi$, and $\psi$ is constant on $H$-conjugacy classes by hypothesis. So $\psi(h^{-1} y h) = \psi(y)$ for $y \in H$. Outside $H$, both $\mathring{\psi}(h^{-1} y h)$ and $\mathring{\psi}(y)$ equal $0$ by definition of the zero extension, so they match directly.
**Contrast with $G$-conjugation.** $\mathring{\psi}$ is generally **not** invariant under $G$-conjugation: if $g \in G \setminus H$ and $y \in H$, then $g^{-1} y g$ may lie outside $H$, in which case $\mathring{\psi}(g^{-1} y g) = 0$ while $\mathring{\psi}(y) = \psi(y)$ may be non-zero. This asymmetry is precisely why we average over all of $G$ in the definition of $\operatorname{Ind}^G_H \psi$ — to symmetrise.
[/guided]
[/step]
[step:Collapse the inner sum over $h$ to obtain the transversal formula]
By Step 3 applied to $y = t_i^{-1} g\, t_i \in G$ (an arbitrary element, not necessarily in $H$),
\begin{align*}
\mathring{\psi}\bigl(h^{-1}(t_i^{-1} g\, t_i)\, h\bigr) = \mathring{\psi}(t_i^{-1} g\, t_i)
\end{align*}
for every $h \in H$. The summand on the right-hand side of the formula in Step 2 is therefore independent of $h$. Summing the constant value $\mathring{\psi}(t_i^{-1} g\, t_i)$ over $h \in H$ yields $|H|$ copies:
\begin{align*}
\sum_{h \in H} \mathring{\psi}\bigl(h^{-1} (t_i^{-1} g\, t_i)\, h\bigr) = |H|\cdot \mathring{\psi}(t_i^{-1} g\, t_i).
\end{align*}
Substituting into the expression from Step 2,
\begin{align*}
\operatorname{Ind}^G_H \psi(g) = \frac{1}{|H|} \sum_{i=1}^n |H|\cdot \mathring{\psi}(t_i^{-1} g\, t_i) = \sum_{i=1}^n \mathring{\psi}(t_i^{-1} g\, t_i),
\end{align*}
which is the transversal formula. This completes the proof.
[/step]
