命題
K を実数体または複素数体とする。
F を K 上のBanach空間(過去スレ008の550)とする。
[a, b] を実数体の有限閉区間とする。
f を [a, b] で定義された F における区分的に C^1 級の曲線(>>327)とする。

このとき f は長さ(>>329)をもち、その長さは ∫[a, b] |f’(x)| dx に等しい。

証明
f は区分的に C^1 級(>>326)であるから、
[a, b] の分点 a = t_0 ＜ t_1 ＜ . . . ＜ t_n = b があり、
f’(t) は各区間 [t_(i-1), t_i] で C^1 級(>>325)である。

f を各区間 [t_(i-1), t_i] に制限した写像を f_i とする。
>>338より、各 f_i は長さをもち、
その長さ L_i は ∫[t_(i-1), t_i] |f’(x)| dx に等しい。

>>333より、f は長さ L をもち、L = ΣL_i である。

他方、>>341より、
∫[a, b] f’(x) dx = Σ∫[t_(i-1), t_i] f’(x) dx である。

よって、L = ∫[a, b] |f’(x)| dx となる。
証明終