過去スレ014の820は複素数体上でも同様に成り立つ：

補題
K を実数体または複素数体とする。
F を K 上のノルム空間とする。

f: [a, b] → F を連続写像とする。
f が (a, b) で微分可能で (a, b) 上で f’(t) = 0 とする。
ここで、f’(t) は>>7で定義したもの。

このとき f は [a, b] 上で定数である。

証明
ある t ∈ [a, b] に対して f(t) ≠ f(a) とする。
Hahn-Banachの定理の系(過去スレ006の755)より、
連続線形写像 g: F → K で、g(f(t)) ≠ g(f(a)) となるものが存在する。

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

よって、
d(gf)(t)(1) = dg(f(t))df(t)(1)
即ち
(gf)’(t) = dg(f(t))f’(t) = 0

よって、>>16より、gf は定数である。
これは、g(f(t)) ≠ g(f(a)) に矛盾である。

よって、f は [a, b] 上で定数である。
証明終