∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] {𝕜 : Type u_4} [inst_3 : NormedRing 𝕜] [inst_4 : Module 𝕜 E]
  [inst_5 : IsBoundedSMul 𝕜 E] (f : C(α, E)) (a : α), ((ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜) f) a = f a