∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_3} [inst : MeasurableSpace β]
  {X Y : Ω → β} [inst_1 : NormedDivisionRing β] [BorelSpace β],
  ProbabilityTheory.IndepFun X Y μ →
    MeasureTheory.Integrable X μ → MeasureTheory.Integrable Y μ → MeasureTheory.Integrable (X * Y) μ