∀ {σ : Type u_1} (R : Type u_2) [inst : DecidableEq σ] [inst_1 : CommSemiring R] (n : σ →₀ ℕ) (x y : MvPowerSeries σ R),
  MvPowerSeries.truncFun' n (x + y) = MvPowerSeries.truncFun' n x + MvPowerSeries.truncFun' n y