∀ {ι : Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] {E : ι → Type u_3}
  [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace ℝ (E i)]
  {L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ} (x y : StrongDual ℝ ((i : ι) → E i)),
  ((ContinuousLinearMap.diagonalStrongDualPi✝ L).toBilinForm x) y =
    ∑ i,
      ((L i).toBilinForm (ContinuousLinearMap.comp x (ContinuousLinearMap.single ℝ E i)))
        (ContinuousLinearMap.comp y (ContinuousLinearMap.single ℝ E i))