∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {ι' : Type u_3} {F : ι' → Type u_2}
  [inst_1 : (i' : ι') → SeminormedAddCommGroup (F i')] [inst_2 : (i' : ι') → NormedSpace 𝕜 (F i')] (i : ι'),
  SMulCommClass 𝕜 𝕜 (F i)