∀ {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] [inst_6 : CompleteSpace A] [inst_7 : NormedSpace ℝ A] (f : X → 𝕜 → 𝕜)
  (a : A),
  (∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 a)) →
    MeasureTheory.Integrable (fun x => ContinuousMap.mkD ((spectrum 𝕜 a).restrict (f x)) 0) μ →
      autoParam (p a) cfc_integral'._auto_1 → cfc (fun z => ∫ (x : X), f x z ∂μ) a = ∫ (x : X), cfc (f x) a ∂μ