∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  [CompleteSpace 𝔸],
  ∀ x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius, Summable fun n => (NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x