{α : Type u_1} →
  [inst : TopologicalSpace α] →
    {R : Type u_2} →
      [inst_1 : CommSemiring R] →
        {A : Type u_3} →
          [inst_2 : TopologicalSpace A] →
            [inst_3 : Semiring A] → [Algebra R A] → [inst_5 : IsTopologicalSemiring A] → R →+* C(α, A)