∀ {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : ProbabilityTheory.Kernel X X} {B : Set X} {f : X → ENNReal},
  π.IsProper →
    𝓑 ≤ 𝓧 →
      Measurable f → MeasurableSet B → ∀ (x₀ : X), ∫⁻ (x : X) in B, f x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f x ∂π x₀