∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {f' : E →L[𝕜] 𝔸}
  {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x →
    ∀ (n : ℕ) (f_1 : Nat.below n),
      HasFDerivWithinAt (fun x => f x ^ n) (∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • f') s
        x