∀ (𝕜 : Type u_1) (A : Type u_2) [inst : CommRing 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : IsTopologicalRing 𝕜]
  [inst_3 : TopologicalSpace A] [inst_4 : Semiring A] [inst_5 : Algebra 𝕜 A] (a b : A),
  { toFun := fun φ => φ (a + b), continuous_toFun := ⋯ } =
    { toFun := fun φ => φ a, continuous_toFun := ⋯ } + { toFun := fun φ => φ b, continuous_toFun := ⋯ }