∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] {f g : α →₀ M}
  {h : α → M → N},
  (∀ (a : α), h a 0 = 0) → (∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) → (f + g).sum h = f.sum h + g.sum h