: 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. $$

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.