# HG changeset patch
# User Andreas Lochbihler
# Date 1361968984 -3600
# Node ID c48477e76de5ff8c7875da9a661149921e033728
# Parent  8c15e50aedadf6cdec2347aa788779747060c596
added lemma

diff -r 8c15e50aedad -r c48477e76de5 src/HOL/Finite_Set.thy
--- 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)