∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {C : ℝ},
  DifferentiableOn ℝ f (Set.Icc 0 1) → (∀ x ∈ Set.Ico 0 1, ‖derivWithin f (Set.Icc 0 1) x‖ ≤ C) → ‖f 1 - f 0‖ ≤ C