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