∀ {Ω : Type u_7} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {M : Type u_10} [inst : AddMonoid M]
  [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M] {f g : Ω → M},
  Measurable f →
    Measurable g →
      MeasureTheory.SigmaFinite (MeasureTheory.Measure.map f μ) →
        MeasureTheory.SigmaFinite (MeasureTheory.Measure.map g μ) →
          ProbabilityTheory.IndepFun f g μ →
            MeasureTheory.Measure.map (f + g) μ = (MeasureTheory.Measure.map f μ).conv (MeasureTheory.Measure.map g μ)