--- 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>