Theorem: Faà di Bruno's Formula

Let $D_x^k u$ denote the $k$th derivative of a function $u$ {{WRT|Differentiation}} $x$.
Then:
:$\ds D_x^n w = \sum_{j \mathop = 0}^n D_u^j w \sum_{\substack {\sum_{p \mathop \ge 1} k_p \mathop = j \\ \sum_{p \mathop \ge 1} p k_p \mathop = n \\ \forall p \mathop \ge 1: k_p \mathop \ge 0} } n! \prod_{m \mathop = 1}^n \dfrac {\paren {D_x^m u}^{k_m} } {k_m! \paren {m!}^{k_m} }$

Proof:
The proof proceeds by induction on $n$.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds D_x^n w = \sum_{j \mathop = 0}^n D_u^j w \sum_{\substack {\sum_{p \mathop \ge 1} k_p \mathop = j \\ \sum_{p \mathop \ge 1} p k_p \mathop = n \\ \forall p \mathop \ge 1: k_p \mathop \ge 0} } n! \prod_{m \mathop = 1}^n \dfrac {\paren {D_x^m u}^{k_m} } {k_m! \paren {m!}^{k_m} }$
The case for $n = 0$ is:
{{:Faà di Bruno's Formula/Example/0}}
which is consistent with the definition of the zeroth derivative.
The case for $n = 1$ is:
{{:Faà di Bruno's Formula/Example/1}}
which is consistent with Derivative of Composite Function.
=== Basis for the Induction ===
$\map P 2$ is the case:
{{:Faà di Bruno's Formula/Example/2}}
This is consistent with Derivative of Composite Function: Second Derivative.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that, if $\map P r$ is true, where $r \ge 2$, then it logically follows that $\map P {r + 1}$ is true.
So this is the induction hypothesis:
:$\ds D_x^r w = \sum_{j \mathop = 0}^r D_u^j w \sum_{\substack {\sum_{p \mathop \ge 1} k_p \mathop = j \\ \sum_{p \mathop \ge 1} p k_p \mathop = r \\ \forall p \mathop \ge 1: k_p \mathop \ge 0} } r! \prod_{m \mathop = 1}^r \dfrac {\paren {D_x^m u}^{k_m} } {k_m! \paren {m!}^{k_m} }$
from which it is to be shown that:
:$\ds D_x^{r + 1} w = \sum_{j \mathop = 0}^{r + 1} D_u^j w \sum_{\substack {\sum_{p \mathop \ge 1} k_p \mathop = j \\ \sum_{p \mathop \ge 1} p k_p \mathop = r \mathop + 1 \\ \forall p \mathop \ge 1: k_p \mathop \ge 0} } \paren {r + 1}! \prod_{m \mathop = 1}^{r + 1} \dfrac {\paren {D_x^m u}^{k_m} } {k_m! \paren {m!}^{k_m} }$
=== Induction Step ===
This is the induction step:
Note that when $k_m = 0$:
:$\dfrac {\paren {D_x^m u}^{k_m} } {k_m! \paren {m!}^{k_m} } = 1$
which shows that any contribution to the summation where $k_m = 0$ can be disregarded.
Let $j = 0$.
Consider the set of $k_p$ such that:
:$k_1 + k_2 + \cdots = 0$
:$1 \times k_1 + 2 k_2 + \cdots = r$
:$k_1, k_2, \ldots \ge 0$
It is apparent by inspection that, for all $r > 0$, no set of $k_p$ can fulfil these conditions.
Therefore when $j = 0$ the summation is vacuous.
Also note that from:
:$1 \times k_1 + 2 k_2 + \cdots = r$
it follows that:
:$k_{r + 1} = k_{r + 2} = \cdots = 0$
Thus, while there are only finitely many $k$'s, their upper limit need not be explicitly considered.
Let $\map c {r, j, k_1, k_2, \ldots}$ be the coefficient of $D_u^j w$ in $D_x^r w$.
We establish some lemmata:
Lemma 1:
{{:Faà di Bruno's Formula/Lemma 1}}
Lemma 2:
{{:Faà di Bruno's Formula/Lemma 2}}
{{finish}}
By differentiating {{WRT|Differentiation}} $x$:
{{begin-eqn}}
{{eqn | l = \map c {r + 1, j, k_1, k_2, \ldots}
      | r = \map c {r, j - 1, k_1 - 1, k_2, \ldots}
      | c = 
}}
{{eqn | o =
      | ro= +
      | r = \paren {k_1 + 1} \map c {r, j, k_1 + 1, k_2 - 1, k_3, \ldots}
      | c = 
}}
{{eqn | o =
      | ro= +
      | r = \paren {k_2 + 1} \map c {r, j, k_1, k_2 + 1, k_3 - 1, k_4, \ldots}
      | c = 
}}
{{eqn | o =
      | ro= +
      | r = \cdots
      | c = 
}}
{{end-eqn}}
The equations:
:$k_1 + k_2 + \cdots = j$
and:
:$k_1 + 2 k_2 + \cdots = r$
are preserved by this induction step.
Thus it is possible to factor out:
:$\dfrac {r!} {k_1! \paren {1!}^{k_1} \cdots k_r! \paren {r!}^{k_r} }$
from each term on the {{RHS}} of the equation for $\map c {r + 1, j, k_1, k_2, \ldots}$.
Thus we are left with:
:$k_1 + 2 k_2 + 3 k_3 + \cdots = r + 1$
So $\map P r \implies \map P {r + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\ds \forall n \in \Z_{\ge 0}: D_x^n w = \sum_{j \mathop = 0}^n D_u^j w \sum_{\substack {\sum_{p \mathop \ge 1} k_p \mathop = j \\ \sum_{p \mathop \ge 1} p k_p \mathop = n \\ \forall p \mathop \ge 1: k_p \mathop \ge 0} } n! \prod_{m \mathop = 1}^n \dfrac {\paren {D_x^m u}^{k_m} } {k_m! \paren {m!}^{k_m} }$