∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : MulOneClass R]
  [inst_3 : BoundedMul R] [inst_4 : ContinuousMul R],
  BoundedContinuousFunction.instMulOneClass =
    { toOne := BoundedContinuousFunction.instOne, toMul := BoundedContinuousFunction.instMul, one_mul := ⋯,
      mul_one := ⋯ }