∀ {σ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] {s : Finset (σ →₀ ℕ)} [inst_1 : CommSemiring S]
  (f : R →+* S) (p : MvPowerSeries σ R),
  (MvPowerSeries.truncFinset S s) ((MvPowerSeries.map f) p) = (MvPolynomial.map f) ((MvPowerSeries.truncFinset R s) p)