∀ (𝕜 : Type u_3) {α : Type u_1} {β : Type u_2} [inst : SeminormedCommRing 𝕜] [inst_1 : SeminormedRing β]
  [inst_2 : Algebra 𝕜 β] [inst_3 : IsBoundedSMul 𝕜 β] (l : Filter α) (f g : α → β),
  f ∈ Filter.boundedFilterSubmodule 𝕜 l →
    g ∈ Filter.boundedFilterSubmodule 𝕜 l → f * g ∈ Filter.boundedFilterSubmodule 𝕜 l