∀ {α : Type u_2} {R : Type u_1} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : Mul R]
  [BoundedMul R] (f g : BoundedContinuousFunction α R), ∃ C, ∀ (x y : α), dist ((⇑f * ⇑g) x) ((⇑f * ⇑g) y) ≤ C