Commuting nearby group elements have commuting logarithms under the stated domain hypotheses

The map $(g,Y)\mapsto {\mathrm{Ad}}_{g}Y$ is continuous and equals $Y$ at $g=e$. Shrink the logarithm neighborhood so that $Y$ and ${\mathrm{Ad}}_{g}Y$ both lie in its exponential chart whenever $g,h\in U$ and $Y={\log }_{G}h$. Since the power series $D({\mathrm{ad}}_X)$ depends continuously on $X$ and equals $I$ at $X=0$, shrink once more so it is invertible for every $X={\log }_{G}g$.

If $gh=hg$, then $gh{g}^{-1}=h$. With $h={\exp }_{G}Y$, [F2] gives ${\exp }_G({\mathrm{Ad}}_{g}Y)={\exp }_{G}Y$. Both exponents lie in the injectivity domain fixed in step 1.1, so ${\mathrm{Ad}}_{g}Y=Y$.

Write $g={\exp }_{G}X$. By [F2], $(e^{{\mathrm{ad}}_X}-I)Y=0$. The power-series identity $e^A-I=D(A)A$ gives $D({\mathrm{ad}}_X)[X,Y]=0$; invertibility from step 1.1 yields $[X,Y]=0$.

The group is nonempty. In dimensions zero and one the conclusion is automatic. Singular ${\mathrm{ad}}_X$ is allowed because only $D({\mathrm{ad}}_X)$, close to $I$, is inverted. There is no interval, endpoint, metric, or biconditional. ${\mathrm{A}\mathrm{C}}_{\omega }$ is inherited exactly through [F1]–[F3]; finitely many neighborhood shrinkings add no choice.