∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → ENNReal},
  Measurable f →
    ∀ (κ : ProbabilityTheory.Kernel β α) [ProbabilityTheory.IsSFiniteKernel κ] (b : β),
      ∫⁻ (p : α × β), f p ∂(κ.prod ProbabilityTheory.Kernel.id) b = ∫⁻ (a : α), f (a, b) ∂κ b