[proofplan]
We compute the multiplicity of each Specht module $S^\lambda$ inside the induced module. [Frobenius reciprocity](/theorems/2449) identifies this multiplicity with the multiplicity of $S^\mu$ inside the restriction of $S^\lambda$ from $S_n$ to $S_{n-1}$. The [Young branching rule for restriction](/theorems/8443) then says that this multiplicity is exactly one when $\lambda$ is obtained from $\mu$ by adding one box and zero otherwise. Finally, Maschke semisimplicity in characteristic zero upgrades the multiplicity computation to the asserted direct-sum decomposition.
[/proofplan]
[step:Use semisimplicity to reduce the induced module to Specht multiplicities]
Fix a partition $\mu \vdash n-1$. Define the induced $kS_n$-module $M := \operatorname{Ind}^{S_n}_{S_{n-1}} S^\mu$. Since $\operatorname{char}(k)=0$, the characteristic of $k$ does not divide $|S_n|=n!$. Hence, by [citetheorem:8439], the group algebra $kS_n$ is semisimple. Therefore $M$ decomposes as a finite direct sum of irreducible $kS_n$-modules.
Using the characteristic-zero Specht classification for symmetric groups, the irreducible $kS_n$-modules are precisely the Specht modules $S^\lambda$ with $\lambda \vdash n$. Thus there are uniquely determined nonnegative integers $m_\lambda$ such that $M$ is isomorphic to the direct sum, over all partitions $\lambda \vdash n$, of $(S^\lambda)^{\oplus m_\lambda}$. It remains to prove that $m_\lambda=1$ exactly when $\mu \nearrow \lambda$, and $m_\lambda=0$ otherwise.
[/step]
[step:Identify each multiplicity by Frobenius reciprocity]
Let $\lambda \vdash n$. Since Specht modules are absolutely irreducible over characteristic zero, the multiplicity $m_\lambda$ of $S^\lambda$ in $M$ is
\begin{align*}
m_\lambda = \dim_k \operatorname{Hom}_{kS_n}(M,S^\lambda).
\end{align*}
Apply Frobenius reciprocity for finite groups to the standard inclusion $S_{n-1}\le S_n$, the $kS_{n-1}$-module $S^\mu$, and the $kS_n$-module $S^\lambda$. This gives a natural $k$-linear isomorphism
\begin{align*}
\operatorname{Hom}_{kS_n}(\operatorname{Ind}^{S_n}_{S_{n-1}}S^\mu,S^\lambda) \cong \operatorname{Hom}_{kS_{n-1}}(S^\mu,\operatorname{Res}^{S_n}_{S_{n-1}}S^\lambda).
\end{align*}
Therefore
\begin{align*}
m_\lambda = \dim_k \operatorname{Hom}_{kS_{n-1}}(S^\mu,\operatorname{Res}^{S_n}_{S_{n-1}}S^\lambda).
\end{align*}
[guided]
The induced module is a module for the larger group $S_n$, but the known branching rule describes what happens when a Specht module for $S_n$ is restricted to $S_{n-1}$. Frobenius reciprocity is exactly the bridge between these two directions.
Fix $\lambda \vdash n$. Since the characteristic-zero Specht modules are irreducible and absolutely irreducible, the multiplicity of $S^\lambda$ in the semisimple module $M=\operatorname{Ind}^{S_n}_{S_{n-1}}S^\mu$ is measured by the dimension of the Hom-space from $M$ to $S^\lambda$: $m_\lambda=\dim_k\operatorname{Hom}_{kS_n}(M,S^\lambda)$. We now apply Frobenius reciprocity for finite groups. Its hypotheses are satisfied because $S_{n-1}$ is a subgroup of the finite group $S_n$, $S^\mu$ is a $kS_{n-1}$-module, and $S^\lambda$ is a $kS_n$-module. The theorem gives a natural isomorphism $\operatorname{Hom}_{kS_n}(\operatorname{Ind}^{S_n}_{S_{n-1}}S^\mu,S^\lambda) \cong \operatorname{Hom}_{kS_{n-1}}(S^\mu,\operatorname{Res}^{S_n}_{S_{n-1}}S^\lambda)$. Taking dimensions over $k$ gives $m_\lambda=\dim_k \operatorname{Hom}_{kS_{n-1}}(S^\mu,\operatorname{Res}^{S_n}_{S_{n-1}}S^\lambda)$. This has converted the desired induction multiplicity into a restriction multiplicity, which is the direction controlled by the Young branching rule for restriction.
[/guided]
[/step]
[step:Apply the restriction branching rule to compute the Hom-space]
The hypotheses of [citetheorem:8443] are satisfied: $k$ has characteristic zero, $\lambda \vdash n$, and $S_{n-1}\le S_n$ is the standard subgroup fixing $n$. Therefore the restriction of $S^\lambda$ to $S_{n-1}$ decomposes as the direct sum, over all partitions $\nu \vdash n-1$ satisfying $\nu \nearrow \lambda$, of $S^\nu$. Here $\nu \nearrow \lambda$ means that $\lambda$ is obtained from $\nu$ by adding exactly one addable box, equivalently that $\nu$ is obtained from $\lambda$ by removing exactly one removable box. Hence $\operatorname{Hom}_{kS_{n-1}}(S^\mu,\operatorname{Res}^{S_n}_{S_{n-1}}S^\lambda) \cong \bigoplus_{\nu \nearrow \lambda}\operatorname{Hom}_{kS_{n-1}}(S^\mu,S^\nu)$. The characteristic-zero Specht modules for $S_{n-1}$ are pairwise non-isomorphic irreducible modules. Therefore [Schur's lemma](/theorems/2414) gives $\dim_k \operatorname{Hom}_{kS_{n-1}}(S^\mu,S^\nu)=1$ if $\nu=\mu$, and $\dim_k \operatorname{Hom}_{kS_{n-1}}(S^\mu,S^\nu)=0$ if $\nu\ne\mu$. Consequently $m_\lambda=1$ if $\mu \nearrow \lambda$, and $m_\lambda=0$ otherwise.
[/step]
[step:Assemble the direct-sum decomposition]
Substituting the computed multiplicities into the semisimple decomposition of $M$ gives $\operatorname{Ind}^{S_n}_{S_{n-1}} S^\mu \cong \bigoplus_{\lambda:\,\mu \nearrow \lambda} S^\lambda$, where $\lambda$ ranges over partitions of $n$. This is exactly the direct sum over all partitions $\lambda$ of $n$ obtained from $\mu$ by adding one addable box, so the Young branching rule for induction follows.
[/step]
