∀ (A : Type u_2) [inst : TopologicalSpace A] [inst_1 : Semiring A] [inst_2 : IsTopologicalSemiring A] {α : Type u_3}
  {β : Type u_1} [inst_3 : TopologicalSpace α] [inst_4 : TopologicalSpace β] (f : C(α, β)) (x x_1 : C(β, A)),
  (x * x_1).comp f = x.comp f * x_1.comp f