∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R] [inst_1 : Nontrivial R]
  [inst_2 : StarRing R] [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R]
  [inst_6 : CommRing S] [inst_7 : Algebra R S] [inst_8 : (i : ι) → NonUnitalRing (A i)]
  [inst_9 : (i : ι) → Module S (A i)] [inst_10 : (i : ι) → Module R (A i)] [∀ (i : ι), IsScalarTower R S (A i)]
  [inst_12 : ∀ (i : ι), SMulCommClass R (A i) (A i)] [inst_13 : ∀ (i : ι), IsScalarTower R (A i) (A i)]
  [inst_14 : (i : ι) → StarRing (A i)] [inst_15 : (i : ι) → TopologicalSpace (A i)] {p : ((i : ι) → A i) → Prop}
  {q : (i : ι) → A i → Prop} [inst_16 : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p]
  [inst_17 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)]
  [∀ (i : ι), ContinuousMapZero.UniqueHom R (A i)] (f : R → R) (a : (i : ι) → A i),
  autoParam (ContinuousOn f (⋃ i, quasispectrum R (a i))) cfcₙ_map_pi._auto_1 →
    autoParam (p a) cfcₙ_map_pi._auto_3 →
      autoParam (∀ (i : ι), q i (a i)) cfcₙ_map_pi._auto_5 → cfcₙ f a = fun i => cfcₙ f (a i)