Universal covering Lie group

The space underlying $G$ is nonempty. It is locally path connected by [F4] and path connected because it is connected. It is semilocally simply connected: for each $g\in G$, choose a coordinate ball $U$ about $g$; after shrinking within a chart, $U$ is contractible, so every loop in $U$ is nullhomotopic in $G$ and the inclusion-induced homomorphism is trivial as in [F5].

By [F1] there is a universal covering map $p:(\tilde{G},\tilde{e})\to (G,e)$. Its total space is simply connected, hence connected, so [F3] gives it the unique Lie-group structure with identity $\tilde{e}$ for which $p$ is a covering homomorphism. This proves existence.

Let $p_i:({\tilde{G}}_i,{\tilde{e}}_i)\to (G,e)$ for $i=1,2$ be two such universal covering Lie groups. By [F2] there is a unique based homeomorphism $F:{\tilde{G}}_1\to {\tilde{G}}_2$ over $G$. In covering charts $F$ is the local expression $(p_2{\mathrm{\mid }}_V{)}^{-1}\circ p_1{\mathrm{\mid }}_U$, so it and its inverse are smooth; hence $F$ is a diffeomorphism.

The maps $F\circ {\tilde{m}}_1$ and ${\tilde{m}}_2\circ (F\times F):{\tilde{G}}_1^2\to {\tilde{G}}_2$ are lifts of the same map $(a,b)\mapsto p_1(a)p_1(b)$ and agree at $({\tilde{e}}_1,{\tilde{e}}_1)$. The domain is connected by [F6], so lift uniqueness [F7] makes the maps equal. Thus $F$ is a Lie-group homomorphism and, being a diffeomorphism, a Lie-group isomorphism.

Any basepoint-preserving Lie-group isomorphism over $G$ is in particular a based continuous map over $G$, so [F2] makes it equal to $F$. This proves the asserted uniqueness. The phrase “over $G$” is essential: without it a simply connected Lie group can have nontrivial identity-preserving automorphisms.