∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [ContinuousStar A] [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [inst_8 : TopologicalSpace X]
  {s : Set 𝕜},
  IsCompact s →
    ∀ (f : 𝕜 → 𝕜) {a : X → A},
      Continuous a →
        (∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s) →
          autoParam (ContinuousOn f s) Continuous.cfcₙ'._auto_1 →
            autoParam (f 0 = 0) Continuous.cfcₙ'._auto_3 →
              autoParam (∀ (x : X), p (a x)) Continuous.cfcₙ'._auto_5 → Continuous fun x => cfcₙ f (a x)