Smooth Inverse Function Theorem on Euclidean Open Sets

Let $n$ be a natural number, let $U$ be an open subset of Euclidean space $\mathbb{R}^n$, and let $f:U\to\mathbb{R}^n$ be a smooth map. Let $a\in U$, and suppose that the Jacobian determinant satisfies $\det J_f(a)\ne 0$. Then there exist open sets $V,W\subseteq\mathbb{R}^n$ with $a\in V\subseteq U$ and $f(a)\in W$ such that $f(V)=W$, the restriction $f|_V:V\to W$ is bijective, and its inverse $h=(f|_V)^{-1}:W\to V$ is smooth. Moreover, the Jacobian matrix of $h$ satisfies $J_h(y)=\bigl(J_f(h(y))\bigr)^{-1}$ for all $y\in W$, where $(\cdot)^{-1}$ denotes the matrix inverse.