∀ {α : Type u} {β : Type v} (𝕜 : Type u_2) [inst : NormedField 𝕜] [inst_1 : TopologicalSpace α] [inst_2 : NormedRing β]
  [inst_3 : NormedAlgebra 𝕜 β] [inst_4 : StarAddMonoid β] [inst_5 : NormedStarGroup β]
  (f : BoundedContinuousFunction α β), ⇑((BoundedContinuousFunction.toContinuousMapStarₐ 𝕜) f) = ⇑f