∀ {σ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S)
  (φ ψ : MvPowerSeries σ R),
  (fun n => f ((MvPowerSeries.coeff n) (φ + ψ))) =
    (fun n => f ((MvPowerSeries.coeff n) φ)) + fun n => f ((MvPowerSeries.coeff n) ψ)