[STATEMENT]
lemma integrable_by_parts_interior:
  fixes prod :: "_ \<Rightarrow> _ \<Rightarrow> 'b :: banach"
  assumes "bounded_bilinear (prod)" "a \<le> b"
          "continuous_on {a..b} f" "continuous_on {a..b} g"
  assumes "\<And>x. x\<in>{a<..<b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
          "\<And>x. x\<in>{a<..<b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
  assumes "(\<lambda>x. prod (f x) (g' x)) integrable_on {a..b}"
  shows   "(\<lambda>x. prod (f' x) (g x)) integrable_on {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. prod (f' x) (g x)) integrable_on {a..b}
[PROOF STEP]
by (rule integrable_by_parts_interior_strong[of _ "{}" _ _ f g f' g']) (insert assms, simp_all)