>>64において E が R 上のBanach空間で、 F が R 上のHilbert空間であれば
f は微分可能で df は p で連続であればよい：

補題
R を実数体とする。
E を R 上のBanach空間とし、
F を R 上のHilbert空間(過去スレ010の600)とする。
E から F への線型写像で位相同型であるもの全体を GL(E, F) と書く。
U を E の開集合とし、f : U → F を微分可能とする。
ある p ∈ U において df は連続であり df(p) ∈ GL(E, F) とする。

このとき、p ∈ V ⊂ U となる開集合 V があり、
f(V) は開集合で、f は V 上で単射である。

証明
>>64の証明において>>62の代わりに>>72を使えばよい。