∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {ι : Type u_2}
  {G : ι → Type u_3} [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)]
  [inst_7 : Fintype ι] {H : Type u_4} [inst_8 : NormedAddCommGroup H] [inst_9 : NormedSpace 𝕜 H]
  [inst_10 : DecidableEq ι] {a : H → E} {a' : H →L[𝕜] E} {b : (i : ι) → H → G i} {b' : (i : ι) → H →L[𝕜] G i}
  {s : Set H} {x : H},
  HasFDerivWithinAt a a' s x →
    (∀ (i : ι), HasFDerivWithinAt (b i) (b' i) s x) →
      ∀ (f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F),
        HasFDerivWithinAt (fun y => (f (a y)) fun i => b i y)
          ((f.flipMultilinear fun i => b i x).comp a' +
            ∑ i, ((f (a x)).toContinuousLinearMap (fun j => b j x) i).comp (b' i))
          s x