diff -r ef195926dd98 -r 8c6747dba731 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Feb 10 12:27:30 2015 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Feb 10 16:08:11 2015 +0000
@@ -262,6 +262,10 @@
   "finite {x. P x} \<Longrightarrow> finite { f x | x. P x }"
   by (simp add: image_Collect [symmetric])
 
+lemma finite_image_set2:
+  "finite {x. P x} \<Longrightarrow> finite {y. Q y} \<Longrightarrow> finite {f x y | x y. P x \<and> Q y}"
+  by (rule finite_subset [where B = "\<Union>x \<in> {x. P x}. \<Union>y \<in> {y. Q y}. {f x y}"]) auto
+
 lemma finite_imageD:
   assumes "finite (f ` A)" and "inj_on f A"
   shows "finite A"
@@ -1618,6 +1622,9 @@
    by (force intro: card_mono simp: card_image [symmetric])
 qed
 
+lemma surj_card_le: "finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> card B \<le> card A"
+  by (blast intro: card_image_le card_mono le_trans)
+
 lemma card_bij_eq:
   "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
      finite A; finite B |] ==> card A = card B"