∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {s : Set 𝕜} (m : ℤ) (k : ℕ),
  IsOpen s →
    Set.EqOn (iteratedDerivWithin k (fun y => y ^ m) s) (fun y => (∏ i ∈ Finset.range k, (↑m - ↑i)) * y ^ (m - ↑k)) s