diff -r 40d1c5e7f407 -r 0a5184877cb7 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Sep 19 12:53:30 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Sep 19 17:37:22 2016 +0200
@@ -1989,6 +1989,21 @@
   finally show ?case by simp
 qed simp_all
 
+(* Contributed by Lukas Bulwahn *)
+lemma image_mset_mset_set:
+  assumes "inj_on f A"
+  shows "image_mset f (mset_set A) = mset_set (f ` A)"
+proof cases
+  assume "finite A"
+  from this \<open>inj_on f A\<close> show ?thesis
+    by (induct A) auto
+next
+  assume "infinite A"
+  from this \<open>inj_on f A\<close> have "infinite (f ` A)"
+    using finite_imageD by blast
+  from \<open>infinite A\<close> \<open>infinite (f ` A)\<close> show ?thesis by simp
+qed
+
 
 subsection \<open>More properties of the replicate and repeat operations\<close>