∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X Y : Ω → ℝ},
  ProbabilityTheory.IndepFun X Y μ →
    MeasureTheory.AEStronglyMeasurable X μ →
      MeasureTheory.AEStronglyMeasurable Y μ →
        ProbabilityTheory.mgf (X + Y) μ t = ProbabilityTheory.mgf X μ t * ProbabilityTheory.mgf Y μ t