∀ {M : Type u_2} {ι : Type u_1} (R : Type u_3) [inst : CommSemiring R] (f : M → ι) (i : ι) {a b : AddMonoidAlgebra R M},
  a ∈ {a | ∀ m ∈ a.support, f m = i} → b ∈ {a | ∀ m ∈ a.support, f m = i} → ∀ m ∈ (a + b).support, f m = i