[STATEMENT]
lemma integral_mult_right_zero[simp]:
  fixes c :: "_::{real_normed_field,second_countable_topology}"
  shows "(\<integral> x. c * f x \<partial>M) = c * integral\<^sup>L M f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. c * f x = c * integral\<^sup>L M f
[PROOF STEP]
by (rule integral_bounded_linear'[OF bounded_linear_mult_right bounded_linear_mult_right[of "1 / c"]]) simp