補題
K を実数体または複素数体とする。
E, Fを K 上のノルム空間とする。
U を E の開集合とし、f: U → F を r 回微分可能とする。
(v_1, ..., v_(r-1)) を固定して
g: U → F を g(x) = (d^(r-1))f(x)(v_1, ..., v_(r-1)) で定義する。

このとき、g は微分可能で、v ∈ E に対して、
dg(x)(v) = (d^r)f(x)(v, v_1, ..., v_(r-1))

証明
ψ: L(E^(r-1), F) → F を T → T(v_1, ..., v_(r-1)) により定義する。
ψ は線型写像であるから微分可能であり、
S ∈ L(E^(r-1), F), T ∈ L(E^(r-1), F) のとき、
dψ(S)(T) = T(v_1, ..., v_(r-1)) である。

h(x) = (d^(r-1))f(x) とおく。

合成関数の微分規則(過去スレ014の803)より、
x ∈ U
v ∈ E のとき、
d(ψh)(x)(v) = dψ(h(x))dh(x)(v)
= (d^r)f(x)(v, v_1, ..., v_(r-1))

一方、
d(ψh)(x)(v) = dg(x)(v)
証明終