∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NormedRing A] [inst_3 : StarRing A] [inst_4 : NormedAlgebra 𝕜 A]
  [inst_5 : ContinuousFunctionalCalculus 𝕜 A p] [CompleteSpace A] [inst_7 : TopologicalSpace X] [OpensMeasurableSpace X]
  {s : Set X},
  MeasurableSet s →
    ∀ (f : X → 𝕜 → 𝕜) (bound : X → ℝ) (a : A) [SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)],
      ContinuousOn (Function.uncurry f) (s ×ˢ spectrum 𝕜 a) →
        (∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x) →
          MeasureTheory.HasFiniteIntegral bound (μ.restrict s) →
            autoParam (p a) integrableOn_cfc._auto_1 → MeasureTheory.IntegrableOn (fun x => cfc (f x) a) s μ