∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {X : Type u_6} [inst_2 : TopologicalSpace X] [FirstCountableTopology X] {F : X → α → G}
  {bound : α → ℝ} {s : Set X},
  (∀ x ∈ s, MeasureTheory.AEStronglyMeasurable (F x) μ) →
    (∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a) →
      MeasureTheory.Integrable bound μ →
        (∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => F x a) s) → ContinuousOn (fun x => ∫ (a : α), F x a ∂μ) s