∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : AddCommMonoid γ] (g h : (i : ι) → β i →+ γ),
  (DFinsupp.sumAddHom fun i => g i + h i) = DFinsupp.sumAddHom g + DFinsupp.sumAddHom h