∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] [inst_2 : DecidableEq α]
  (f : α →₀ M) (a : α) (b : α → M → N),
  (f.sum fun x v => if a = x then b x v else 0) = if a ∈ f.support then b a (f a) else 0