∀ {ι : Type u_1} {γ : Type u_3} {β : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : AddCommMonoid γ] (x : (i : ι) → β i →+ γ),
  (fun F i => F.comp (DFinsupp.singleAddHom β i)) (DFinsupp.sumAddHom x) = x