Globalising a homomorphism defined on a ball

Let $V$ be a real normed vector space (a normed additive commutative group with a compatible $\mathbb{R}$-module structure), let $A$ be a group, let $r$ be a real number with $0 < r$, and let $e_0 : V \to A$ be an arbitrary function, subject to the single hypothesis that $e_0$ is additive-to-multiplicative wherever all three arguments lie in the open ball of radius $r$: for all $v, w \in V$ with $\lVert v\rVert < r$, $\lVert w\rVert < r$ and $\lVert v + w\rVert < r$ one has $e_0(v + w) = e_0(v)\,e_0(w)$. The conclusion asserts that there exists a unique monoid homomorphism $e : \mathrm{Multiplicative}\,V \to A$ — that is, a homomorphism from the additive group of $V$ written multiplicatively, into $A$ — such that $e(\mathrm{ofAdd}\,v) = e_0(v)$ for every $v \in V$ with $\lVert v\rVert < r$. Uniqueness is uniqueness in the sense of ExistsUnique: any monoid homomorphism agreeing with $e_0$ on the ball of radius $r$ equals $e$. No topology or continuity is imposed on $A$, and no continuity of $e_0$ is assumed.

This is the standard globalisation of a local homomorphism defined on a ball of a real normed space: since the ball generates the additive group and the space is divisible, a partial homomorphism extends uniquely to the whole group. It is used in the construction of the complex uniformisation of abelian varieties, where the global exponential map is obtained from a locally defined one; it is cited by GoodReductionJacobian.AbelianSchemePropertyBundle.exists_submodule_pointEquiv_quotient_differentiableOn_appLE.