Lemma 1

Let G be a Lie group, U an open neighbourhood of e, E a complete normed space and $\phi : U \to E$ a chart of the manifold G. There exists a neighbourhood W of e contained in U such that $\phi | W$ is an isomorphism of W (with the right uniform structure) onto $\phi(W)$ (with the uniform structure induced by that on E).

It can be assumed that $\phi(e) = 0$. Let $U' = \phi(U)$. Let $\psi : U' \to U$ be the inverse mapping of $\phi$. Let V be a symmetric open neighbourhood of e such that $V^2 \subset U$ and let $V' = \phi(V)$. We define mappings $\theta_1, \theta_2$ of $V' \times V'$ into $V' \times U'$ as follows:

It is immediately verified that $\theta_2(\theta_1(x, y)) = \theta_1(\theta_2(x, y)) = (x, y)$ for $x, y$ sufficiently close to 0. On the other hand, $\theta_1$ and $\theta_2$ are analytic and hence strictly differentiable at $(0, 0)$. Therefore (Differentiable and Analytic Manifolds, R, 1.2.2) there exist a neighbourhood $W'$ of 0 in $V'$ and constants $a > 0, b > 0$ such that

for all $x_1, x_2, y_1, y_2$ in $W'$. Writing $x_1 = x_2 = y_2$, we obtain

For $\delta > 0$, let $N_\delta$ be the set of ordered pairs $(x, y) \in W' \times W'$ such that $\| x - y \| \leq \delta$. The $N_\delta$ form a fundamental system of entourages in $W'$. We write $W = \psi(W')$. Let $M_\delta$ be the set of ordered pairs $(u, v) \in W \times W$ such that $\| \phi(uv^{-1}) \| \leq \delta$. The $M_\delta$ form a fundamental system of entourages in $W$ with the right uniform structure. But relation (2) proves that

and hence $W$ has the property of the lemma.