∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {X : Type u_5} {Y : Type u_6}
  [inst_2 : TopologicalSpace X] [inst_3 : TopologicalSpace Y] [inst_4 : MeasurableSpace X] [inst_5 : MeasurableSpace Y]
  [OpensMeasurableSpace X] [OpensMeasurableSpace Y] {f : X → Y → E},
  Continuous (Function.uncurry f) →
    HasCompactSupport (Function.uncurry f) →
      ∀ {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsFiniteMeasureOnCompacts μ]
        [MeasureTheory.IsFiniteMeasureOnCompacts ν],
        ∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ = ∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν