過去スレ014の828は F が複素Banach空間でも同様に成り立つ：

命題
K を実数体または複素数体とする。
E を K 上のノルム空間とし、F を K 上のBanach空間とする。
U を E の開集合とし、f: U → F をC^1級写像とする。

V を R の開集合で [0, 1] ⊂ V とする。
ψ: V → U をC^1級写像とする。
x = ψ(0), y = ψ(1) とする。

このとき
f(y) - f(x) = ∫[0, 1] df(ψ(t))(ψ’(t)) dt

証明
g(t) = f(ψ(t)) とおく。

合成関数の微分法(過去スレ014の803)より、
dg(t) = df(ψ(t))dψ(t)
よって、
dg(t)(1) = df(ψ(t))dψ(t)(1)

>>7より、
g’(t) = df(ψ(t))(ψ’(t))

>>18より、
f(y) - f(x) = ∫[0, 1] g’(t) dt = ∫[0, 1] df(ψ(t))(ψ’(t)) dt
証明終