∀ (α : Type u_1) [inst : TopologicalSpace α] (R : Type u_2) [inst_1 : CommSemiring R] [inst_2 : TopologicalSpace R]
  [inst_3 : IsTopologicalSemiring R] [Subsingleton α], Subsingleton (Subalgebra R C(α, R))