diff -r f35aa0e7255d -r b33803fcae2a src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Sat Jun 16 07:13:17 2018 +0200
+++ b/src/HOL/Transitive_Closure.thy	Sat Jun 16 20:32:00 2018 +0200
@@ -659,6 +659,13 @@
    apply (auto simp add: finite_Field)
   done
 
+lemma finite_rtrancl_Image: assumes "finite R" "finite A" shows "finite (R\<^sup>* `` A)"
+proof (rule ccontr)
+  assume "infinite (R\<^sup>* `` A)"
+  with assms show False
+    by(simp add: rtrancl_trancl_reflcl Un_Image del: reflcl_trancl)
+qed
+
 text \<open>More about converse \<open>rtrancl\<close> and \<open>trancl\<close>, should
   be merged with main body.\<close>