∀ {M : Type u_2} {R : Type u_6} [inst : Semiring R] {N : Type u_8} [inst_1 : AddZeroClass N]
  {f g : MonoidAlgebra R M →+ N},
  f = g ↔ ∀ (m : M), f.comp (MonoidAlgebra.singleAddHom m) = g.comp (MonoidAlgebra.singleAddHom m)