∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : AddCommMonoid γ] (f : (i : ι) → β i →+ γ) (i : ι),
  (DFinsupp.liftAddHom f).comp (DFinsupp.singleAddHom β i) = f i