∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : Monoid M] {S : Set (MonoidAlgebra R M)},
  Algebra.adjoin R S = ⊤ → Algebra.adjoin R (⋃ f ∈ S, ⇑(MonoidAlgebra.of R M) '' ↑f.support) = ⊤