C^1 級関数 F : R^n × U →　R^n を

(2.6) F(y, x) = f(x) - y

によって定義する。このとき

(2.7) F(b, a) = 0

である。さらに

(2.8) det ∂F/∂x(y, x) = det f'(x)

であるから、仮定(2.4)により

(2.9) det ∂F/∂x(b, a) ≠ 0

である。(2.7), (2.9)により F は陰関数定理の仮定をみたす。
したがって、点 a, b の開近傍 V (⊂ U), W と、 C^1 級関数 g : W → V 存在して、次の(2.10), (2.11)をみたす。ただし f(V) = W とする。

(2.10) g(b) = a
(2.11) x ∈ V, y ∈ W に対して、 y = f(x) ⇔ x = g(y).