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