∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) (n : ℕ) (s : Set ℝ) (x₀ : ℝ),
  taylorWithin f (n + 1) s x₀ =
    taylorWithin f n s x₀ +
      (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀))
        ((PolynomialModule.single ℝ (n + 1)) (taylorCoeffWithin f (n + 1) s x₀))