Pick a point . There is an such that is a diffeomorphism of the ball (the tangent space) into . Since is a homeomorphism, is an open set in and .

Now, since is an isometry, for all geodesics -\delta,\delta)\rightarrow N" alt="\gamma-\delta,\delta)\rightarrow N" /> with , for the geodesic -\eta,\eta)\rightarrow M" alt="\beta-\eta,\eta)\rightarrow M" /> with and , we have that

This means exists (for all of the tangent space, as is complete); and since is complete, we can consider the map defined by This is a diffeomorphism, and inverse to the (restricted map) . So is a diffeomorphism.

Note. I do not see why this would not work if was only a local isometry.

Note 2. Thin Lizzy - Whiskey in the jar