∀ {ι : Type u_3} {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {V : ι → Submodule 𝕜 E} {i : ι},
  V i ≠ ⊥ → 0 < Module.finrank 𝕜 ↥(V i)