∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedSpace ℝ E]
  [inst_6 : NormedSpace ℝ F] {a b : E} {s : Set E} {ω : E → E →L[𝕜] F} {dω : E → E →L[ℝ] E →L[𝕜] F} [CompleteSpace F],
  Convex ℝ s →
    (∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x) →
      (∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x) →
        a ∈ s → b ∈ s → HasFDerivWithinAt (fun x => ∫ᶜ (x : E) in Path.segment a x, ω x) (ω b) s b