diff -r 69ee23f83884 -r 8260d8971d87 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Apr 12 09:18:36 2023 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Apr 12 19:56:05 2023 +0200
@@ -3257,6 +3257,28 @@
   shows "monotone (multp orda) (multp ordb) (image_mset f)"
   by (rule monotone_on_multp_multp_image_mset[OF assms, simplified])
 
+lemma multp_image_mset_image_msetI:
+  assumes "multp (\<lambda>x y. R (f x) (f y)) M1 M2" and "transp R"
+  shows "multp R (image_mset f M1) (image_mset f M2)"
+proof -
+  from \<open>transp R\<close> have "transp (\<lambda>x y. R (f x) (f y))"
+    by (auto intro: transpI dest: transpD)
+  with \<open>multp (\<lambda>x y. R (f x) (f y)) M1 M2\<close> obtain I J K where
+    "M2 = I + J" and "M1 = I + K" and "J \<noteq> {#}" and "\<forall>k\<in>#K. \<exists>x\<in>#J. R (f k) (f x)"
+    using multp_implies_one_step by blast
+
+  have "multp R (image_mset f I + image_mset f K) (image_mset f I + image_mset f J)"
+  proof (rule one_step_implies_multp)
+    show "image_mset f J \<noteq> {#}"
+      by (simp add: \<open>J \<noteq> {#}\<close>)
+  next
+    show "\<forall>k\<in>#image_mset f K. \<exists>j\<in>#image_mset f J. R k j"
+      by (simp add: \<open>\<forall>k\<in>#K. \<exists>x\<in>#J. R (f k) (f x)\<close>)
+  qed
+  thus ?thesis
+    by (simp add: \<open>M1 = I + K\<close> \<open>M2 = I + J\<close>)
+qed
+
 lemma multp_image_mset_image_msetD:
   assumes
     "multp R (image_mset f A) (image_mset f B)" and