∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {m : Type u_7} {n : Type u_8} [inst_3 : Fintype n] [inst_4 : DecidableEq n] [inst_5 : Fintype m]
  (b : OrthonormalBasis n 𝕜 E) (b₂ : OrthonormalBasis m 𝕜 𝕜) (x : E),
  (LinearMap.toMatrix b.toBasis b₂.toBasis) ((innerₛₗ 𝕜) x) = Matrix.vecMulVec (star ⇑b₂) (star (b.repr x).ofLp)