--- a/src/HOL/Finite_Set.thy Wed Feb 27 10:33:45 2013 +0100
+++ b/src/HOL/Finite_Set.thy Wed Feb 27 13:43:04 2013 +0100
@@ -356,6 +356,16 @@
"finite A \<Longrightarrow> (\<And>a. a\<in>A \<Longrightarrow> finite (B a)) ==> finite (SIGMA a:A. B a)"
by (unfold Sigma_def) blast
+lemma finite_SigmaI2:
+ assumes "finite {x\<in>A. B x \<noteq> {}}"
+ and "\<And>a. a \<in> A \<Longrightarrow> finite (B a)"
+ shows "finite (Sigma A B)"
+proof -
+ from assms have "finite (Sigma {x\<in>A. B x \<noteq> {}} B)" by auto
+ also have "Sigma {x:A. B x \<noteq> {}} B = Sigma A B" by auto
+ finally show ?thesis .
+qed
+
lemma finite_cartesian_product:
"finite A \<Longrightarrow> finite B \<Longrightarrow> finite (A \<times> B)"
by (rule finite_SigmaI)