∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (M : ι → Type u_2) [inst_2 : (i : ι) → AddCommMonoid (M i)]
  (M' : Type u_3) [inst_3 : AddCommMonoid M'] (φ : ((i : ι) → M i) →+ M'),
  (fun φ => ∑ i, (φ i).comp (Pi.evalAddMonoidHom M i)) ((fun φ i => φ.comp (AddMonoidHom.single M i)) φ) = φ