∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {S₁ : Type u_5} {S₂ : Type u_6} [inst_1 : CommSemiring S₁]
  [inst_2 : CommSemiring S₂] (f : R →+* S₁) (g : S₁ →+* S₂) (p : MvPowerSeries σ R),
  (MvPowerSeries.map g) ((MvPowerSeries.map f) p) = (MvPowerSeries.map (g.comp f)) p