: Seja $f : U \subset \mathbb{R}^m \rightarrow \mathbb{R}^m$ uma função $C^r, 1 \leq r \leq \infty$ e suponhamos que $Df_p$ é inversível para algum $p \in U$ (aberto), então $f$ é um difeomorfismo $C^r$ de uma vizinhança de $p$ a sua imagem, i.e existe $ V \subset U$ contendo $p$ tal que a restrição $f : V \rightarrow f(V)$ é inversível e sua inversa também é diferenciável.

Demonstração: Seja $F(x, y) = f(x) - y$. Claro que $F$ é $C^r$ e além disto $F(p, f(p) = 0$ a derivada de $F$ com respeito de $x$ em $p$ é $Df_p$ e portanto inversível. Podemos aplicar teorema função implicita ($x, y$ são trocados com respeito dos enunciado do teorema da função implícita) e escrever $x$ como uma função de $y$, ou seja existe uma função $h : V \rightarrow U_0$ tal que $F(h(y), y) =0$ e portanto $$ f(h(y))=y , f \circ h = id|V. $$

Ist mostra que $h$ é uma inversa direita para $f$. Para provar que $h$ define uma função inversa local para $f$ basta mais um pouco de trabalho e usando que $h$ obtida pelo Teorema função implícita é única:

Seja $U_1 = \{x \in U_0, f(x) \in V\}$ vamos mostrar que:

1. $U_1$ é uma vizinhança de $p$
2. $h$ é uma inversa direita de $f|_{U_1}$ i.e, $f|_{U_1} \circ h = id|_{V}$
3. $h$ é inversa esquerda de $f|_{U_1}$ i.e, $h \circ f|_{U_1} = id|_{U_1}$

Para (1) observe que pela continuidade da $f$ e $V$ ser um conjunto aberto, concluímos que $U_1$ é aberto. Para provar (2), seja $y \in V$ então $h(y) \in U_0, f(h(y))=y$ e portanto $h(y) \in U_1$ e portanto $f|_{U_1} \circ h$ é bem definida e é identidade em $V$.

Finalmente para (3) tomamos $x \in U_1,$ pela definição $f(x) \in V$ e existe ´¨nico ponto $h(f(x)) \in U_0$ tal que $F(h(f(x)), f(x))=0$ , mas sabemos que $F(x, f(x))=0$ e portanto pela unicidade temos que $h(f(x))=x$.