∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} [inst_3 : Fintype ι] {V : ι → Submodule 𝕜 E} [inst_4 : ∀ (i : ι), CompleteSpace ↥(V i)],
  (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) → ∀ x ∈ iSup V, ∑ i, (V i).starProjection x = x