∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {s : Finset (σ →₀ ℕ)},
  IsLowerSet ↑s →
    ∀ {x : σ →₀ ℕ} (f g : MvPowerSeries σ R),
      x ∈ s →
        MvPolynomial.coeff x ((MvPowerSeries.truncFinset R s) f * (MvPowerSeries.truncFinset R s) g) =
          (MvPowerSeries.coeff x) (f * g)