[STATEMENT]
lemma integrable_mult_indicator:
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  shows "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> sets M; integrable M f\<rbrakk> \<Longrightarrow> integrable M (\<lambda>x. indicat_real A x *\<^sub>R f x)
[PROOF STEP]
by (rule integrable_bound[of M f]) (auto split: split_indicator)