∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] (F : α → M →+ N)
  (x x_1 : α →₀ M), ((x + x_1).sum fun x => ⇑(F x)) = (x.sum fun x => ⇑(F x)) + x_1.sum fun x => ⇑(F x)