∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_7} {n : ℕ} {x : 𝕜} {f : ι → 𝕜 → F} {I : Finset ι} {s : Set 𝕜},
  x ∈ s →
    UniqueDiffOn 𝕜 s →
      (∀ i ∈ I, ContDiffWithinAt 𝕜 (↑n) (f i) s x) →
        iteratedDerivWithin n (fun x => ∑ i ∈ I, f i x) s x = ∑ i ∈ I, iteratedDerivWithin n (f i) s x