[STATEMENT]
lemma prime_elem_multiplicity_prod_mset_distrib:
  assumes "prime_elem p" "0 \<notin># A"
  shows   "multiplicity p (prod_mset A) = sum_mset (image_mset (multiplicity p) A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity p (\<Prod>\<^sub># A) = \<Sum>\<^sub># (image_mset (multiplicity p) A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime_elem p
(0::'a) \<notin># A

goal (1 subgoal):
 1. multiplicity p (\<Prod>\<^sub># A) = \<Sum>\<^sub># (image_mset (multiplicity p) A)
[PROOF STEP]
by (induction A) (auto simp: prime_elem_multiplicity_mult_distrib)