∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] [NoZeroDivisors R] [Nontrivial R] {ι : Type u_4} (w : σ → ℕ)
  (f : ι → MvPowerSeries σ R) (s : Finset ι),
  MvPowerSeries.weightedOrder w (∏ i ∈ s, f i) = ∑ i ∈ s, MvPowerSeries.weightedOrder w (f i)